{"entities":{"Q43945":{"pageid":44001,"ns":120,"title":"Item:Q43945","lastrevid":105428423,"modified":"2026-10-09T10:09:47Z","type":"item","id":"Q43945","labels":{"en":{"language":"en","value":"Simpl"}},"descriptions":{"en":{"language":"en","value":"AFP entry Simpl"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"79982b32842de61e8a74f269c89e74250fbc9661","datavalue":{"value":"32234","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43945$CAF0ABB7-9279-41E2-B72C-AE99DC63C6A2","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":"Q43945$9CC05DA3-0AD3-4376-AAA8-ED5F6ED06EEB","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"a6fc4bb71bdab8f30d7f9c5dbe67d958eefe8c98","datavalue":{"value":"https://www.isa-afp.org/entries/Simpl.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q43945$EEF3564B-5A54-46D3-8AB1-558690CDC2BD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43945$CCE42FAB-FC43-4087-9037-D3A3BA086068","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"14c1585ec43c4b9edf59fbea0f64f76002c1f698","datavalue":{"value":{"entity-type":"item","numeric-id":43914,"id":"Q43914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$5F0F9182-CFFF-422E-8E65-8B5155943A1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ea53781dc0a29ca150a09c3de99800e897e49297","datavalue":{"value":{"entity-type":"item","numeric-id":40507,"id":"Q40507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$F2419CB5-FD6C-40DF-BC1B-C01F0F34D0F2","rank":"normal"},{"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":"Q43945$E727927E-A4A6-444E-B57E-E1A0F0D0B9D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"d4f9ffd0ab91ebc6a95d22ce0096cbfcb2f4e17a","datavalue":{"value":{"entity-type":"item","numeric-id":33628,"id":"Q33628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$7A8E242A-8A24-4C8A-9A7F-96B612BF12B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$970CB153-BE19-4299-AEC2-1342F40A8014","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ce995af0d54f8ab3594278c155d6ae4d6e3a6165","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$37267FCA-4F98-4528-ADBE-106D606F81EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"263af5c0df32ed66fc675fae4932e71337532265","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$81030FAD-EBEB-40C0-96F1-8FBE2F8CF457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e09694fe3792b5d00306e3d52d45d5816179ce38","datavalue":{"value":{"entity-type":"item","numeric-id":21688,"id":"Q21688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$BEB7D111-A732-4444-8739-E87FF8730AA6","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":"Q43945$3793FB3E-B30C-4BA8-9E54-815A54F3F329","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"24f3341d2ed9d75827488c61b9cd6e1237e02358","datavalue":{"value":"https://isa-afp.org/entries/Simpl.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q43945$AC5F485C-2D24-4D90-9D37-21745E82C880","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"45e860162f4b3c0ff9ec8446d8b1743804a3a1b4","datavalue":{"value":"Norbert Schirmer","type":"string"},"datatype":"string"},"type":"statement","id":"Q43945$B5DBA9F0-C2DC-4E6D-8CF2-01A41D4E1311","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fea5c4486e1e2eb5894a1dbc9b35a42edd7ed496","datavalue":{"value":"We present the theory of Simpl, a sequential imperative programming language. We introduce its syntax, its semantics (big and small-step operational semantics) and Hoare logics for both partial as well as total correctness. We prove soundness and completeness of the Hoare logic. We integrate and automate the Hoare logic in Isabelle/HOL to obtain a practically usable verification environment for imperative programs. Simpl is independent of a concrete programming language but expressive enough to cover all common language features: mutually recursive procedures, abrupt termination and exceptions, runtime faults, local and global variables, pointers and heap, expressions with side effects, pointers to procedures, partial application and closures, dynamic method invocation and also unbounded nondeterminism.","type":"string"},"datatype":"string"},"type":"statement","id":"Q43945$9161A6D0-D35B-4768-A7B4-6F3E44E8820A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6db1a4e5dc42421c546d4010b6ec0e33d7f4d940","datavalue":{"value":{"entity-type":"item","numeric-id":5458324,"id":"Q5458324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$66249FF9-17AE-44E1-B03F-7FB86C9C64E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a655377852f4fbc1e40cdceec18686655bda680","datavalue":{"value":{"entity-type":"item","numeric-id":5712320,"id":"Q5712320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$92280D36-2010-48DF-81DD-E5410B8669A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b04e0182b28454a7b199f37533b58d86266395f9","datavalue":{"value":{"entity-type":"item","numeric-id":704168,"id":"Q704168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$C13E7693-1E0C-475A-86B4-CBB2455BEE16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"447080a77c9018e473151c503e22f493141efe68","datavalue":{"value":{"entity-type":"item","numeric-id":5900714,"id":"Q5900714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$B3E0C0AE-730A-4C50-906B-B155EC625D2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c7fe4f7bbdf41a15f375fda905d86bb957912ea","datavalue":{"value":{"entity-type":"item","numeric-id":4247084,"id":"Q4247084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$CC4D56EA-09B2-4EB9-B3C7-32D3E4D9FBF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$CF899F7C-D602-4DBF-99EB-E2CD8F2E6A09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d46dcc76189e927a9b701aff09df28b0631368a","datavalue":{"value":{"entity-type":"item","numeric-id":5477661,"id":"Q5477661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$19B43B7A-A105-4ECD-A3B7-49FA482AD79F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2819bd996a82604201d8aab0900cbc265825a6b6","datavalue":{"value":{"entity-type":"item","numeric-id":2369295,"id":"Q2369295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$E8744831-2A75-4A5C-8E4A-EC24CFC7391E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19d68f92fffaefe72b592d24843b2770631f989c","datavalue":{"value":{"entity-type":"item","numeric-id":3189788,"id":"Q3189788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$8E893A80-4097-473E-90F8-672C77959E8E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8713d2dcfa9d1a073646ef1961a1cffe50b69332","datavalue":{"value":{"time":"+2008-02-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q43945$430ED0BB-C092-4E57-8163-4DA4D78661CD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c86d09a72dc02529ac047f694c255b56d652bd15","datavalue":{"value":{"text":"A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q43945$394AE04E-2DE9-40F4-82F9-33FB9F73F0EF","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":"Q43945$BBEFCE0F-C379-4B61-927F-3FC775C8A43D","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"9beb5f7be6b27e22c4af581585b828086bbf7950","datavalue":{"value":{"entity-type":"item","numeric-id":7360796,"id":"Q7360796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43945$DE680BF1-3A1D-4372-A334-A3F4E5BC5B0C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Simpl (AFP entry Simpl)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Simpl_(AFP_entry_Simpl)"}}}}}