{"entities":{"Q1122978":{"pageid":1133727,"ns":120,"title":"Item:Q1122978","lastrevid":66816135,"modified":"2026-04-12T13:03:08Z","type":"item","id":"Q1122978","labels":{"en":{"language":"en","value":"A language independent proof of the soundness and completeness of generalized Hoare logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4108141"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$E1466F3B-EC58-4E9B-A0FF-8B1081AC73F3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7b26992ccdb2a3fc7aa6e9622754cac5fc25133f","datavalue":{"value":{"text":"A language independent proof of the soundness and completeness of generalized Hoare logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1122978$A29A7D54-A4B0-4CDA-A139-2BA54370DF7B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3e12ee594b4e7480fb970b512162124a267f61ad","datavalue":{"value":"0676.68004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122978$FBED521F-66D1-4716-BBBB-06B9D77C2E1C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fe6e612654a76139218f1a394e9776e339cc53b9","datavalue":{"value":"10.1016/0890-5401(89)90018-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122978$A4F2005A-24D6-4BEC-879D-B50985C14D21","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"66475c89deaa1b82e2a733011ec9769bb2327168","datavalue":{"value":{"entity-type":"item","numeric-id":655408,"id":"Q655408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$452812AB-415A-4D5C-B480-EF7C3FC9AC54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"aabe6d988e05fe3a7b00666b4b0ee76e06b180c4","datavalue":{"value":{"entity-type":"item","numeric-id":655409,"id":"Q655409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$934AD799-B477-441E-96EA-C94F3078C4B6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$87AC158E-BCFB-443F-A491-1B9AD7118D24","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1122978$8991CFCB-DAD4-416F-8CE5-07918165479D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4efd7aae621f5313850555d0de56f4caec76be35","datavalue":{"value":"For generalized Hoare logic (GHL), a formal system for proving invariance properties of programs was introduced in papers of \\textit{L. Lamport} [Acta Inf. 14, 21-37 (1980; Zbl 0416.68032)] and \\textit{L. Lamport}, \\textit{F. B. Schneider} [ACM Trans. Program. Lang. Syst. 6, 281-296 (1984; Zbl 0536.68017)]. The authors first give a rigorous definition essentially independent of any programming language. Then they describe a corresponding semantic, introduce a suitable consequence relation, and prove for the provability relation of GHL its soundness as well as its (relative) completeness with respect to that consequence relation.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1122978$A1CDD79B-A24C-4C9B-AE41-A8C810B04941","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122978$2EFEEAF6-9E04-4074-92AD-1F32BCCB9D6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122978$BBB595AA-F22F-4879-9C15-7D19D9C11F7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122978$B0A57B00-79E5-4206-9316-E916D5D5B09E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f6c507238b78450d52d27e6a8341341542bcd8d5","datavalue":{"value":"4108141","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122978$5FC79A4B-95C0-4BF8-A59B-A8CF172FF929","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bf07a2dfb7bfd7a74614dd83c9c97ddb71d46530","datavalue":{"value":"program verificiation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1122978$B778BD2A-ED4E-4624-BA5C-39FD280621BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3300d494d834018bd4caaa8717cf9394d7055b92","datavalue":{"value":"reasoning about programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1122978$539AB3CA-65E6-458D-9107-7688E95D5C29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1122978$0BA07B9B-6EA8-425F-8641-B417EEF5FE92","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"d657b6d3412c75416b1faf0735572c94c2285816","datavalue":{"value":{"entity-type":"item","numeric-id":586246,"id":"Q586246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$350C1D12-A516-4C94-BBB2-3413C4898871","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$B779FD1E-DD89-44D0-8F10-847C2DF9A308","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"834b7b82319faf201c5c5ea605beeec5a9d61eed","datavalue":{"value":"https://doi.org/10.1016/0890-5401(89)90018-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q1122978$532BE866-F8BD-4C51-B93B-00D5F31DACBA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6529053c70f59c18345b2c357253ed5aea3e6e53","datavalue":{"value":"W2014375692","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122978$B84540D0-3319-4A1E-A6E9-5FC678E58444","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3bc80122c3248b7370a66f915205122d19550f7","datavalue":{"value":{"entity-type":"item","numeric-id":3925144,"id":"Q3925144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$773D498F-B3D2-450C-99D3-9810EBA54676","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f640c010e86f562d69961f36d8777ab01b6e3073","datavalue":{"value":{"entity-type":"item","numeric-id":1056534,"id":"Q1056534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$37A48878-A4C0-4AB3-870A-1242CA059F96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c166cfe0e3a05c6a84e2be26185c9beeb7d177c9","datavalue":{"value":{"entity-type":"item","numeric-id":1215264,"id":"Q1215264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$BBBE9C8E-0002-4829-8357-1F67ABCAD62D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2c71c26bf7e075dc23cee40b3135f1af13e67a2","datavalue":{"value":{"entity-type":"item","numeric-id":4151703,"id":"Q4151703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$0DEAB2A3-3B9B-4C45-B7C9-D8ACDC1EB9B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6130a72bad290e99b4d30823cf592f64ef05b4a8","datavalue":{"value":{"entity-type":"item","numeric-id":5584402,"id":"Q5584402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$D051E938-0172-4FAA-9263-3DB4A400CC93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$8AC1A47F-F0E3-4717-9F3A-AD4484C8EA19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e3a418fbaddcafed1884dac6bf4b839b94ad4db","datavalue":{"value":{"entity-type":"item","numeric-id":754637,"id":"Q754637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$4C63E6DD-43B5-48D8-8BCA-F096532D7C7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b68d01684c688b76f9852f57744d277bca068de","datavalue":{"value":{"entity-type":"item","numeric-id":3321433,"id":"Q3321433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$21FC8FD5-B7C7-4C00-A285-4BDACA8B7064","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"377324767631186c74643cd4927092bc831167c8","datavalue":{"value":{"entity-type":"item","numeric-id":4139636,"id":"Q4139636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122978$860FAA45-BA4A-4AE3-8573-C448B75AC144","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec691ca6b94f8362541f7a20d08563e9b7b24d68","datavalue":{"value":{"entity-type":"item","numeric-id":1107518,"id":"Q1107518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"910daaa3bbf1b814542ab545426a4e36a4145044","datavalue":{"value":{"amount":"+0.8371567726135254","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1122978$E377ED33-E85E-4D33-AE71-A956C7E7F871","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"580d88c695e564f75837432b6f488bd75e374497","datavalue":{"value":{"entity-type":"item","numeric-id":3321433,"id":"Q3321433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c852a59a4b76fa10b7022eebec2aa79f9d259cdb","datavalue":{"value":{"amount":"+0.8218356370925903","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1122978$F1D86800-887C-4E77-81ED-A68FBD7D6C7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e2201ceba745f8f4bc88d73a6cab694ed61248d5","datavalue":{"value":{"entity-type":"item","numeric-id":794426,"id":"Q794426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"342441e1e95ea919b6ab3200a0d22aa5798bc3f2","datavalue":{"value":{"amount":"+0.8081793189048767","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1122978$612911D7-1713-446D-BB28-97E941A73464","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fd5c2832aabbf4b304824c9b3020a0ed9253b4e","datavalue":{"value":{"entity-type":"item","numeric-id":4823141,"id":"Q4823141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2da0d3952b5b4ff1d32ee658164caaef3f6f051c","datavalue":{"value":{"amount":"+0.7955575585365295","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1122978$918B1673-BD0F-49F7-873D-698E88496776","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00a02dd3cc93ca3c9a0e16106fae253dc2e0af80","datavalue":{"value":{"entity-type":"item","numeric-id":1602554,"id":"Q1602554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa43fd1a9fbb63879d628efbdcba265c4f5c9ecb","datavalue":{"value":{"amount":"+0.787790060043335","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1122978$59C65592-D739-42F9-BDCC-73679B7FCE7D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A language independent proof of the soundness and completeness of generalized Hoare logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_language_independent_proof_of_the_soundness_and_completeness_of_generalized_Hoare_logic"}}}}}