{"entities":{"Q40949":{"pageid":41005,"ns":120,"title":"Item:Q40949","lastrevid":105427463,"modified":"2026-10-09T10:07:39Z","type":"item","id":"Q40949","labels":{"en":{"language":"en","value":"Imperative Refinement"}},"descriptions":{"en":{"language":"en","value":"AFP entry Refine_Imperative_HOL"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"4095a732cec1f29d920ee8c79936e5e95bdcf13a","datavalue":{"value":"29235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40949$D26707DE-14A5-4974-8DA3-B3448D33ED22","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":"Q40949$3D905934-4773-413B-B66B-98119742B723","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"e00c5b1299b54ef786a61b4006f65feb4283355c","datavalue":{"value":"https://www.isa-afp.org/entries/Refine_Imperative_HOL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40949$F03FF696-7877-42EE-8CF9-C8BB1D272A21","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"95bde9084e6ca63a8492631a417b047b22c72453","datavalue":{"value":"05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40949$E4D20A62-7DE7-4AC8-9BA7-7BB0799821B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40949$81F31714-C44D-48D2-8DA4-94493F5D1173","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d524cbea14b3375266fe3893cb26a33f13ae791e","datavalue":{"value":"5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40949$19768C3E-DCBB-4B05-A83E-75E95F9244FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40949$32C9A501-46E6-4639-B592-74D912C629CD","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":"Q40949$6CF90D5B-5728-46EB-86BE-E707AC5522D2","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":"Q40949$3AE7FDF7-0F6A-41CF-BAAB-3144F8FADB19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$CC44B4BF-7015-4645-BA6F-1F374F659FFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"27b35591f9a1d87570b3e9ffb19e51ff7cd09a28","datavalue":{"value":{"entity-type":"item","numeric-id":40544,"id":"Q40544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$DEA81AB8-584F-409A-9D7A-2D67359CDCBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a5226fd137c2167e439294ca4cdc09da6fe13411","datavalue":{"value":{"entity-type":"item","numeric-id":40324,"id":"Q40324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$3E160E7A-DC38-4008-BA53-3A64A9D79180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ac6e4b2309e3317f96b1f72a4f626411283f5bc5","datavalue":{"value":{"entity-type":"item","numeric-id":40629,"id":"Q40629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$5AFE3E67-CAC7-4A71-A92F-4849F708AC24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"587eb1ff352d74d75ec39594cac10abdfc1440c2","datavalue":{"value":{"entity-type":"item","numeric-id":40265,"id":"Q40265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$1DC9A029-022F-487E-9FF0-FE0B9FACC425","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4eea1e5549472c93f3282a38917960fdec6b61a1","datavalue":{"value":{"entity-type":"item","numeric-id":24733,"id":"Q24733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$D67805EB-0D64-48E2-954E-184B3AB5F30C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$40E119AD-114B-4539-9DD3-5D6C06B3B29F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4dfac822d106dc7f697754008c4906d0b5156921","datavalue":{"value":{"entity-type":"item","numeric-id":35396,"id":"Q35396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$9A9F51CF-53BC-439B-8CBC-C20B5966E64A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9c92f90cbb18601fb0e3e567e9d0ef7714554113","datavalue":{"value":{"entity-type":"item","numeric-id":38696,"id":"Q38696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$27D48D53-4618-4CA5-A619-9EFB851A0DBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1d9a241ea62c19819316dc010d562c6313b3903b","datavalue":{"value":{"entity-type":"item","numeric-id":25228,"id":"Q25228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$BB5D02A3-A62D-49A2-BCB1-A32216FE16DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"36dacd5e0ce6f221a0ecf90efa0c07a5dd9417fd","datavalue":{"value":{"entity-type":"item","numeric-id":19839,"id":"Q19839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$8830F831-5C2F-4D05-8677-D83D6CB86725","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e37d0f84800bb830b88b7439acea2ef09d22c165","datavalue":{"value":{"entity-type":"item","numeric-id":13366,"id":"Q13366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$92D2BD09-0781-4323-A43F-763D50FC0DA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"07eb0f28b45c8f9b5cf112bbf02e95717fb938ca","datavalue":{"value":{"entity-type":"item","numeric-id":25202,"id":"Q25202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$7C2D4166-AE03-4F1A-A0C2-1CEFDD698D65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"73bdf83b845075653e4f87bf9bebb10f97ebc7d2","datavalue":{"value":{"entity-type":"item","numeric-id":26832,"id":"Q26832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$5380BABD-C4DF-4AFD-85E0-AC517E31A302","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"845fea984bd3d6706acc856d0595755051e72c0c","datavalue":{"value":{"entity-type":"item","numeric-id":40263,"id":"Q40263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$15A5F5C4-E524-45F2-9BB6-5F3DDF75977F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b82155c8d1da98891c9daad267405a7d93979d3b","datavalue":{"value":{"entity-type":"item","numeric-id":33165,"id":"Q33165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$45B04F3E-4382-4F88-97A5-C529470F7A7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ccca80b6de24b80a4ce2a4ab4e48d31e9686f36a","datavalue":{"value":{"entity-type":"item","numeric-id":40262,"id":"Q40262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$712BD2BA-E03E-4460-93C0-00BDFBA24A11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$3235702A-584B-40AA-88B7-58101FF77869","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7fea90d497c9e7d376cb60b753106390234edf13","datavalue":{"value":"https://isa-afp.org/entries/Refine_Imperative_HOL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40949$E579C6A0-A519-4B4C-A71F-2E64DBC2BE9A","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7545c5768cca6bd4b47e52bfec18c22cb81849df","datavalue":{"value":"Peter Lammich","type":"string"},"datatype":"string"},"type":"statement","id":"Q40949$AD28EEBA-966F-42C7-BEB4-E25A28E2B477","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b1c9103c7a13e81077bcfd02abd0d9973d610a2e","datavalue":{"value":"We present the Imperative Refinement Framework (IRF), a tool that supports a stepwise refinement based approach to imperative programs. This entry is based on the material we presented in [ITP-2015, CPP-2016]. It uses the Monadic Refinement Framework as a frontend for the specification of the abstract programs, and Imperative/HOL as a backend to generate executable imperative programs. The IRF comes with tool support to synthesize imperative programs from more abstract, functional ones, using efficient imperative implementations for the abstract data structures. This entry also includes the Imperative Isabelle Collection Framework (IICF), which provides a library of re-usable imperative collection data structures. Moreover, this entry contains a quickstart guide and a reference manual, which provide an introduction to using the IRF for Isabelle/HOL experts. It also provids a collection of (partly commented) practical examples, some highlights being Dijkstra's Algorithm, Nested-DFS, and a generic worklist algorithm with subsumption. Finally, this entry contains benchmark scripts that compare the runtime of some examples against reference implementations of the algorithms in Java and C++. [ITP-2015] Peter Lammich: Refinement to Imperative/HOL. ITP 2015: 253--269 [CPP-2016] Peter Lammich: Refinement based verification of imperative data structures. CPP 2016: 27--36","type":"string"},"datatype":"string"},"type":"statement","id":"Q40949$041402F2-DAAE-4A81-8EEE-420AFF04D73E","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"f0d6ccc9a00d2d1e3be7ec2239689671c14dec25","datavalue":{"value":{"entity-type":"item","numeric-id":7361918,"id":"Q7361918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$4A897A6E-82BA-43F7-8FE3-65FD497DCCBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c0e4b154d3cbaa6adcd084b741855073f781fcfd","datavalue":{"value":{"entity-type":"item","numeric-id":7361011,"id":"Q7361011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$AFCDFD86-3CBD-4225-805B-5F15D9F41799","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"dc69b5476b22ddcb06553e82ecc431ee41932a0e","datavalue":{"value":{"entity-type":"item","numeric-id":7361202,"id":"Q7361202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$CD94D320-883C-457E-BF71-B8DBD882F19F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"e0b5465b6a0d9e05645cdb7168eee1aaf7eb2845","datavalue":{"value":{"entity-type":"item","numeric-id":7361518,"id":"Q7361518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$F3ED7951-5F81-40AE-9EE0-4D2CBC979605","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"a2692e956d33db26682a093f2137dfbe53eccbae","datavalue":{"value":{"entity-type":"item","numeric-id":7361251,"id":"Q7361251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$4FF6929B-36FD-44E1-AD61-1CBF5FCD279A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1cacbaa0ec3f11c9f9035239c4493ecb9bac4b64","datavalue":{"value":{"time":"+2016-08-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40949$73EC4A9A-7F54-431B-8533-AC556F9A962B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9923e5e1039d550cc6f844d6d1b8de2a86e822c1","datavalue":{"value":{"text":"The Imperative Refinement Framework","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40949$A6681E1D-3DA8-4AB9-B5C1-0CA54A243575","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":"Q40949$B5E1AF6D-DFC6-4510-AA92-36BDAB032628","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"65dbfb47d0b5da65bd2cdfbc8cab28721a9f7690","datavalue":{"value":{"entity-type":"item","numeric-id":7360803,"id":"Q7360803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40949$FC50563B-A2DF-4254-8CB7-3D6E583F12A4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Imperative Refinement","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Imperative_Refinement"}}}}}