{"entities":{"Q7361107":{"pageid":31518860,"ns":120,"title":"Item:Q7361107","lastrevid":105423368,"modified":"2026-10-08T13:45:15Z","type":"item","id":"Q7361107","labels":{"en":{"language":"en","value":"Program Construction and Verification Components Based on Kleene Algebra"}},"descriptions":{"en":{"language":"en","value":"AFP entry Algebraic_VCs"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4171002971269ae923bc537465f6d24bfff5f513","datavalue":{"value":"https://isa-afp.org/entries/Algebraic_VCs.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361107$3BE97B1C-64E4-4688-96B1-45ADC7104C79","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"cebadfd7b78bd04e93befe8d7c5151d4488b7f71","datavalue":{"value":"Victor B. F. Gomes","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361107$CDF79313-869C-4A29-BF12-E30F36E7F6B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"791c9af3f632028a8094f425e13128d157950d83","datavalue":{"value":"Georg Struth","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361107$0AEE714D-0232-48B8-8071-D1727D8BF06A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"78a4147215f10ab50a1b13bd3d15f0388137ecb5","datavalue":{"value":"Variants of Kleene algebra support program construction and verification by algebraic reasoning. This entry provides a verification component for Hoare logic based on Kleene algebra with tests, verification components for weakest preconditions and strongest postconditions based on Kleene algebra with domain and a component for step-wise refinement based on refinement Kleene algebra with tests. In addition to these components for the partial correctness of while programs, a verification component for total correctness based on divergence Kleene algebras and one for (partial correctness) of recursive programs based on domain quantales are provided. Finally we have integrated memory models for programs with pointers and a program trace semantics into the weakest precondition component.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361107$984BCD4E-34B3-4E17-8D5E-866100EFE914","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"42767904ec698e77bf5ad5a5ca09192ebfa305eb","datavalue":{"value":{"entity-type":"item","numeric-id":2941173,"id":"Q2941173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$983E2A88-0585-40AA-9A16-E08CF03CCC08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc62f32ebe5f2c566c09500f98ee202c262830a","datavalue":{"value":{"entity-type":"item","numeric-id":736461,"id":"Q736461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$BB68743A-596D-4912-A629-59E6B075D63E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13b2e611a60bbb1cbb1ab23d8301e40dbbe2b3c5","datavalue":{"value":{"entity-type":"item","numeric-id":2915136,"id":"Q2915136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$208A2796-7E55-4B9E-9A0C-E142EFED3808","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c21563ebfe4989a0c68d86523017377bbcfc1cb","datavalue":{"value":{"entity-type":"item","numeric-id":406433,"id":"Q406433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$26B76C62-9327-4952-99E5-465778C6ADB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79e807f14dcd5f9ad4f6bbeb1f8ea3c4bbb7d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":4396958,"id":"Q4396958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$6C52534F-A778-40CD-8B8C-61C3A5B3CFC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c95887997d61befa174dc6f5c2a08804d32a7d64","datavalue":{"value":{"entity-type":"item","numeric-id":5639639,"id":"Q5639639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$0A688D3F-7534-497E-99BB-C11E20793C99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c08dc42b0e7ff775d175e9650bc18837bb9e6bc1","datavalue":{"value":{"entity-type":"item","numeric-id":5277765,"id":"Q5277765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$FF5E818D-E125-4728-AFEF-9DE13D8A3C2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87c7893913ac74b7ec3bad95e74075ab9512b7bf","datavalue":{"value":{"entity-type":"item","numeric-id":3003302,"id":"Q3003302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$E0127F06-7D90-4B82-9B16-882D9BA8D5BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d5703d8b9ac3f2ec42c5cea3cb6310bb02f051a","datavalue":{"value":{"entity-type":"item","numeric-id":627202,"id":"Q627202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$0DB1A63D-FB97-43C2-BE67-59303BC0A9EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed0f96bd7644b87078b54e3f53823b650999a057","datavalue":{"value":{"entity-type":"item","numeric-id":3163399,"id":"Q3163399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$C538E9A1-670F-4A0D-9A0E-57B9F078361E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2790188d3a2572a99d3b8280868598d27c040965","datavalue":{"value":{"entity-type":"item","numeric-id":4525781,"id":"Q4525781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$8A0092E6-6B5E-4A8B-8463-F6227727CEF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b505b8d56ce32f5bd927de5ce0f364ed7bc3b98a","datavalue":{"value":{"entity-type":"item","numeric-id":1371311,"id":"Q1371311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$18BA4BFF-ADFB-4386-8D7A-DC3BE11030CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e13d4d25d9b41b80813e9e3772d78e6f24c19a44","datavalue":{"value":{"entity-type":"item","numeric-id":5738898,"id":"Q5738898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$C43BA63F-5B32-4908-B7C5-5C13405693DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50820dcc1af6c5a368ac6f3fdc4a1d7adb9ffb30","datavalue":{"value":{"entity-type":"item","numeric-id":2767087,"id":"Q2767087"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$F8A9CADB-DBDD-4D83-909E-5011A499D051","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d8a6a7f4a099b96912e5cba667c8ca70d007bb8","datavalue":{"value":{"entity-type":"item","numeric-id":287365,"id":"Q287365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$F134ADE2-7640-46F7-806E-C4E730EC1B67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62386516d9e4edfd13150a63c443c59cb377920e","datavalue":{"value":{"entity-type":"item","numeric-id":820135,"id":"Q820135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$71BF1008-176C-4FCD-95A2-B04DB2D06402","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"768da93377b5dbe67ffc466d796d0d32932c2d63","datavalue":{"value":{"entity-type":"item","numeric-id":4301161,"id":"Q4301161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$1C992B01-23BF-43D4-B532-0F14390B2320","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11015c2590743aa394d6a0295baf2497e9c917c4","datavalue":{"value":{"entity-type":"item","numeric-id":4749182,"id":"Q4749182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$73BC72A9-F1F2-4C86-8D2D-77A365AB311F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e264974062f53b439460b85662778a60b49509d","datavalue":{"value":{"entity-type":"item","numeric-id":2926333,"id":"Q2926333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$3D33F1CE-C78F-4AC4-95FD-8ACAC9D240F3","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":"Q7361107$0FCD81B2-B71F-434D-AC1F-9A3B21519E95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12bcad11fe97484505c727089d3af542344d4df9","datavalue":{"value":{"entity-type":"item","numeric-id":4930176,"id":"Q4930176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$A047EF36-D144-4322-AEA0-EF6F417377C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb9b6fee7afc6e55aa83396b5c6df38a519c39df","datavalue":{"value":{"entity-type":"item","numeric-id":4273477,"id":"Q4273477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$1ED26A93-1616-4142-AA98-AF1550DFD6E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4736b8f52d3360a8824f86f9655f4169ce694d1a","datavalue":{"value":{"entity-type":"item","numeric-id":1931903,"id":"Q1931903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$C9EE731A-6794-415E-961E-E86EC37F4196","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ed2be9418a43957af5bd4e04a6d0289797fc5e2","datavalue":{"value":{"entity-type":"item","numeric-id":903368,"id":"Q903368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$93E6192B-FA55-4EE9-A4CB-0CE1A054060A","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"842345d524917a859fbf25bdbec5eafcad9e81bc","datavalue":{"value":{"entity-type":"item","numeric-id":7361028,"id":"Q7361028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$3F5337D1-A58A-459C-B046-31AE955A6937","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"422342c3fb34631af5f61097819a09568775a669","datavalue":{"value":{"entity-type":"item","numeric-id":7361454,"id":"Q7361454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$E375305C-85AE-413B-A22D-B137C4EA94D0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7e096bb73be3cadbf6ab1a4856c3a6e635fcc69f","datavalue":{"value":{"time":"+2016-06-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361107$3E527207-699D-47D8-ABA2-98CF3316CF28","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"56a0dec5e40f71e9dfe0eb2fe52e5a8ffd1e580c","datavalue":{"value":{"text":"Program Construction and Verification Components Based on Kleene Algebra","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361107$FF82307E-F9B6-43B2-920D-40068413C9DA","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":"Q7361107$73958C1F-1FAA-49C5-9E7A-907B74D71DE7","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"65292b3c42fa1bd5c21e4c91fe94fdc3f630f232","datavalue":{"value":{"entity-type":"item","numeric-id":7360821,"id":"Q7360821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$E36AF86E-9F4C-4577-8DE4-E4D9C252D826","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":"Q7361107$45D01B02-3E1B-4359-BDF3-C8A2EC6B8697","rank":"normal"}],"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"b28f0fab746e0d4e5ff7df48b6fd54d7dedf2848","datavalue":{"value":"32217","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361107$4E387DB6-8FBA-44DF-8685-0737EA7C8472","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361107$1C936EB5-C79E-43E5-AF8C-7E6DBFA870A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361107$3F6C5BEE-E2CF-4FBF-AFB5-16B39F297A47","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":"Q7361107$576A7986-332C-4DC9-AEFC-749EB14A5F6E","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":"Q7361107$ACFB7E50-F802-4EB3-BDB9-36BFFE5D777D","rank":"normal"},{"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":"Q7361107$67E275DE-90AB-4D1C-89D6-70834BA4A6E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"181a8497f7a319d54026dcfccf5a714e5c58403f","datavalue":{"value":{"entity-type":"item","numeric-id":40512,"id":"Q40512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$368E2004-69B6-4400-9FE3-D76A7448DE11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a84cec67941530633e685a8ee56a19ae6a02d7e8","datavalue":{"value":{"entity-type":"item","numeric-id":56258,"id":"Q56258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$2E8CF91D-DB15-4EBB-BB39-A3B8FF1F4175","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f659a0f84020c7c9cd05ca15cec41dfa781088c0","datavalue":{"value":{"entity-type":"item","numeric-id":35704,"id":"Q35704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$41F5E821-29B4-4509-96AB-8D214A07831D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cf16ca8b4217a77a4217a7973bcd79e35c3e2bb9","datavalue":{"value":{"entity-type":"item","numeric-id":5974121,"id":"Q5974121"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$57A9940D-CFD0-4A5F-9DAE-352D23344BFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f37aaa72463d35f8933622cc257886a0465bc696","datavalue":{"value":{"entity-type":"item","numeric-id":5972481,"id":"Q5972481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$313EF37A-7162-41CA-9D27-DB0EA86FAFDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a1718a76c81b10dcc81cbdbe69fc8fe178db7b09","datavalue":{"value":{"entity-type":"item","numeric-id":16299,"id":"Q16299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$2AF88DDF-955A-41D2-8E68-E94C5B08389E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6ea1daaaad60197d0d83fc7ac701579957406893","datavalue":{"value":{"entity-type":"item","numeric-id":16063,"id":"Q16063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$C4A87608-9D42-4922-B22E-09F75891DBF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"09e2993cb5d494a347b340b5a9f971135cd04442","datavalue":{"value":{"entity-type":"item","numeric-id":43942,"id":"Q43942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$09FBA00C-F059-42D7-9B6E-EA2AFA9A9309","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"deb8ff1d94ce91499b3c889ad52e2af0d30c31a1","datavalue":{"value":{"entity-type":"item","numeric-id":43956,"id":"Q43956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$FDC3858D-4FF4-4D3D-ACC9-51FB10376C61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"411138fa9472ce40b1eaa8986ea45be52fe481ce","datavalue":{"value":{"entity-type":"item","numeric-id":18827,"id":"Q18827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$1413A55F-3A6C-4C45-8996-5ADB7A250AD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"255d1eab6148b0a0149f5ba251f819f772375a4c","datavalue":{"value":{"entity-type":"item","numeric-id":23492,"id":"Q23492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$30C14F89-4DBA-4231-B286-BB06F25A667A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c2172a64dbcb79ebade4fc487fb160cecff5b410","datavalue":{"value":{"entity-type":"item","numeric-id":43925,"id":"Q43925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$AA3E1F2E-13A9-4A04-AA09-52A78F66BA70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1cca3a32b180baf92e5c1bd6e47c20bc43d7599e","datavalue":{"value":{"entity-type":"item","numeric-id":32996,"id":"Q32996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361107$5405D008-2AF4-4475-A1B8-8B958EF78006","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":"Q7361107$5AD87638-1EDE-4F9B-97B5-8F1641C3025E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Program Construction and Verification Components Based on Kleene Algebra","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Program_Construction_and_Verification_Components_Based_on_Kleene_Algebra"}}}}}