{"entities":{"Q51732":{"pageid":51788,"ns":120,"title":"Item:Q51732","lastrevid":105426716,"modified":"2026-10-09T10:06:01Z","type":"item","id":"Q51732","labels":{"en":{"language":"en","value":"IMP2_Binary_Heap"}},"descriptions":{"en":{"language":"en","value":"AFP entry IMP2_Binary_Heap"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"11ca75454b812a4ebe10e24ae737c580362b230e","datavalue":{"value":"36030","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q51732$9086FFF9-9B99-4FBD-B514-211B605FBFDE","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$36A277C7-3340-4318-8FBC-597BCE62B16D","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"2450307652debdf334d221695d1dc82b73da1ef9","datavalue":{"value":"https://www.isa-afp.org/entries/IMP2_Binary_Heap.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q51732$B4103446-A9B5-4A70-B9FB-3FE282D03211","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q51732$B1B89BAB-EE18-43BF-B17C-D16317CC6A5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"541da1e359051dfcf3c498b9f1f1f8f905fbafe3","datavalue":{"value":"90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q51732$7CC3C009-EDDA-4801-A0CB-FA449F23188F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a8aa801742e290b2e6820d89349e86d8f23555f","datavalue":{"value":"90.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q51732$8BC63BC5-5388-4745-8CFD-162C150598FD","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$42C79186-417E-43A8-8E10-72344A1F03F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$D689AAD5-0BE1-479E-9F18-71F8FA50EF46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"13de30f88d0d4fe9c5e21ee6f7da73ef297225d7","datavalue":{"value":{"entity-type":"item","numeric-id":30361,"id":"Q30361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$5813DA94-6BC7-46B6-BC2F-2B1CCB16169A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ff80b41d03c65073c007c903a317be0a9c94293e","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$81D69312-51F9-4059-BEEA-A39F283EEB31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f57e49294646f8e693c0de606c6b939c4c4d234a","datavalue":{"value":{"entity-type":"item","numeric-id":40965,"id":"Q40965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$8DBE1239-E7BC-4894-A00E-863DA3D2C3C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4d7f4b76492a75780585d40fb718d00d42a05322","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$E71206A1-D76B-421D-B63C-ED2981F7D6C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4d81d02aeed8be60bec4eae0b793a8c2a2347a49","datavalue":{"value":{"entity-type":"item","numeric-id":46083,"id":"Q46083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$8D53F2AA-7254-4A96-897B-7C4F0242349E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"583675b13be5f1d5d55e9f4b322cf50040e205b1","datavalue":{"value":{"entity-type":"item","numeric-id":44086,"id":"Q44086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$2E6CF3D3-E5FC-4C36-8CB8-64D802139936","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7be4145414c2429f47282433414c638de68f044e","datavalue":{"value":{"entity-type":"item","numeric-id":40904,"id":"Q40904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$7A5DA028-28F5-4365-98C4-D7849CB84F38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"67d5af6ef410bc7cf7f49a8833d90ef52e36c612","datavalue":{"value":{"entity-type":"item","numeric-id":20911,"id":"Q20911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$075C719E-5714-4BD4-B4C2-0F900F1F91DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bc63b18f29e81036c5e8291dd57d82490deaa954","datavalue":{"value":{"entity-type":"item","numeric-id":19233,"id":"Q19233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$0A91726E-B72F-41FF-81EB-4487A16EF4EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"af7596ea90a473f9470e833bf08344ca1ec71143","datavalue":{"value":{"entity-type":"item","numeric-id":40151,"id":"Q40151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$843FE586-4AEB-4889-912C-79C4BAA1514D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2e072a738543502cb1df91e8cb89fd6f06eabadf","datavalue":{"value":{"entity-type":"item","numeric-id":17043,"id":"Q17043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$E566D99D-89B3-44A0-8297-121406A5A25D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"aaf6e75530e1e7514e4aef61310d82e82248ef2b","datavalue":{"value":{"entity-type":"item","numeric-id":55487,"id":"Q55487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$B0C798D5-4EDE-401F-AF3C-545FA50FAAA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"d03c375b1fbbe0a810fb04a9f9434b8658bd9aa7","datavalue":{"value":{"entity-type":"item","numeric-id":21946,"id":"Q21946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$7F68238F-7B84-42E5-9334-32D62535B76E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"d1c96b2bdf2e942a6fc8a55fa9f34649a3e8568c","datavalue":{"value":{"entity-type":"item","numeric-id":46612,"id":"Q46612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$BEFCE454-816A-4AC7-ABE6-7AC85DD8A9E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"271b3d2efaee8f28d411cee9af08d6fb6a3f0193","datavalue":{"value":{"entity-type":"item","numeric-id":21213,"id":"Q21213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$57B6D2A9-EEB3-4201-80A1-9515B48AE903","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"dd25ad249c2b0bfc0ae57f791baa0d6fded59cb3","datavalue":{"value":{"entity-type":"item","numeric-id":32511,"id":"Q32511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$A9125D06-4602-4E1E-A1DF-26F7307B4690","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"392dd935cd270bdf05534c469a4a6d49bfca7156","datavalue":{"value":{"entity-type":"item","numeric-id":16271,"id":"Q16271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$BC4C6614-A9DD-4298-BBAE-AA3EBFE20A29","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fc356816dc9f1e81cbbdeb43908a35e3e0c7e8d9","datavalue":{"value":"https://isa-afp.org/entries/IMP2_Binary_Heap.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q51732$5AA5256C-B582-485A-AF4A-A082074D27C1","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"bc5e5720a8f8636652438250d8ccfb50155e568b","datavalue":{"value":"Simon Griebel","type":"string"},"datatype":"string"},"type":"statement","id":"Q51732$0CA8A8ED-7D53-4B5B-BC66-66186266D3EC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6319382f814205efca69504e0f57f49c5ea2cefc","datavalue":{"value":"In this submission array-based binary minimum heaps are formalized. The correctness of the following heap operations is proved: insert, get-min, delete-min and make-heap. These are then used to verify an in-place heapsort. The formalization is based on IMP2, an imperative program verification framework implemented in Isabelle/HOL. The verified heap functions are iterative versions of the partly recursive functions found in \"Algorithms and Data Structures \u2013 The Basic Toolbox\" by K. Mehlhorn and P. Sanders and \"Introduction to Algorithms\" by T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein.","type":"string"},"datatype":"string"},"type":"statement","id":"Q51732$B3B76D5C-554B-4AA3-A477-708C26DA5ACC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ad76b5dd25eb2fe9929fa11937c74cde9ae1865","datavalue":{"value":{"time":"+2019-06-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q51732$816B67FE-22B5-4FC4-B7AC-51D42AD6642E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"adf810e8a6e18537c12fc300054bacd8b60498d4","datavalue":{"value":{"text":"Binary Heaps for IMP2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q51732$B06A1C11-FCC9-47F8-8A5C-6FD3D2C9B191","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9194e9b150f8488fef979658da21ddd0e60751fc","datavalue":{"value":{"entity-type":"item","numeric-id":3651735,"id":"Q3651735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$1A11B0B2-2476-4500-810F-2050A72B65B2","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$BD3A606D-690A-45AE-897C-0139D44402DA","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"e33b556049348231a1b1107437c5139f0adaf98c","datavalue":{"value":{"entity-type":"item","numeric-id":7361453,"id":"Q7361453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$E9BD8E21-ABA9-45B5-8A8E-E8476C2BD6F9","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ef7bddd24a035fe32f48fd95ea6033928a9b8e67","datavalue":{"value":{"entity-type":"item","numeric-id":7360788,"id":"Q7360788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51732$DBD0BDF5-EAD4-44EA-BCB8-0E7A7E3D44B4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"IMP2 Binary Heap","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/IMP2_Binary_Heap"}}}}}