{"entities":{"Q1124311":{"pageid":1135060,"ns":120,"title":"Item:Q1124311","lastrevid":69841647,"modified":"2026-04-13T10:42:35Z","type":"item","id":"Q1124311","labels":{"en":{"language":"en","value":"Weak second order characterizations of various program verification systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4111981"}},"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":"Q1124311$9147C5B5-37B5-408E-8C88-5548072DB5D5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e8b705bc461e3d4ff77a3c07bfa51de375217681","datavalue":{"value":{"text":"Weak second order characterizations of various program verification systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1124311$2974BD34-DC97-4665-8FD8-CDC498D74884","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8aefc5e29ff657e094a28f4acfd8a68e3ec32c1d","datavalue":{"value":"0678.68008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1124311$6F81B690-37CC-4E51-AFB2-A1AFF70A73CD","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6fe68990767f4dddb98b97060f3b0c3eff8aa4d4","datavalue":{"value":"10.1016/0304-3975(89)90156-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1124311$148440F6-C778-4C2A-B673-654C8846E493","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e46a0c110e220042f8c25f69d7566fe58fbf25b7","datavalue":{"value":{"entity-type":"item","numeric-id":514567,"id":"Q514567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$7CF1D9EB-AA3F-4D09-8ABD-BA5E85634BCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"32ead6a624fee23dc1dc37cfe2dcec3766470899","datavalue":{"value":{"entity-type":"item","numeric-id":452475,"id":"Q452475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$47CFEF67-5E1E-44DE-BA84-3B9E66713955","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$7BFC3407-6B70-49A2-B38D-09CD8AAA3FFC","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":"Q1124311$4D9D2199-463D-4D0C-91B3-97697EE98F89","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"63f89a68d2563fa0d37cd90e5fc7c52f10ffc74c","datavalue":{"value":"Program verification systems like the inductive assertions method by Floyd-Hoare, the intermittent assertions method due to Burstall and the temporal logic of programs attributed to Pnueli are revisited to be compared in verification power by Leivant's characterization based on weak second order logic. Leivant's characterization of the Floyd-Hoare logic is proven equivalent to Csirmaz's and Sain's applying Nonstandard Logics of Programs. Then Burstell's and Pnueli's verification systems are subjected to Leivant's weak second order logic as well.    Thus all systems presented yield characteristic results in reference to the essential comprehension scheme in weak second order logic.    To compare the program verifying powers of different systems one may determine a class of program assertions like partial correctness, total correctness, safety or liveness properties by their first order approximations.    To refine this characterization the authors set out to vary the first order approximation to the partial correctness assertion the way pursued by Leivant but from a different starting point.    Thus they conclude that Leivant's theorem merely states the equivalence of the Floyd-Hoare method to weak second order program verification with a specific comprehension scheme and a specific weak second order approximation of the partial correctness assertion.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1124311$7611AE4D-857C-4060-BB59-04166637B36C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1124311$6A8CEB99-11F5-4590-8D99-4D8720202D3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1124311$15422F07-DC58-4C16-AF89-A5C3FD523257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"89a6721807d2106ad3a18783b4fcbc004e6a56c5","datavalue":{"value":"03B60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1124311$FD5B28C9-9E9C-4E75-9338-2007BF0F989C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5d9cb31903e5e8a60364c2446e17e7d83e318407","datavalue":{"value":"4111981","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1124311$74A427B4-2353-4A88-A97E-94BD68DA8A1B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9928ae9fcfaf03e4706ca2a7e2f249f4a8e042bb","datavalue":{"value":"Program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1124311$A56AD811-BD79-4E4C-B998-7381B5549EDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ea811d864a984b410a67df5fbc1ccbc3b77db799","datavalue":{"value":"second order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1124311$E4C8691B-E81B-4FBC-B5D8-CB0582B8003E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c253cad3eb6a0748a247f5a606eca2b5933e9c0d","datavalue":{"value":"comprehension scheme","type":"string"},"datatype":"string"},"type":"statement","id":"Q1124311$3540E5E0-7EEC-4216-AE2A-6AD1E4DCD85F","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":"Q1124311$1DB375EA-BCB7-4E40-8A8F-1C5D9352C255","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2c0bcc7b5876a552f94708efd58838f43f77bbab","datavalue":{"value":"https://doi.org/10.1016/0304-3975(89)90156-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q1124311$A3938125-02F3-4374-8EB3-3C5E3256DBB1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b464e82b127ced5c59bb1f705c272a2e386a9c85","datavalue":{"value":"W1991123457","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1124311$CA0C179E-DCD1-4DC5-BF20-D9AD6359060F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"423ba48ea0c0081e3c033946437e629a625920c6","datavalue":{"value":{"entity-type":"item","numeric-id":1239727,"id":"Q1239727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$27C4B9DD-9EF9-4DD6-80F8-737BEBFCEF89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95424454d8bc3f84a57ba0475f1936732a8371ae","datavalue":{"value":{"entity-type":"item","numeric-id":4193440,"id":"Q4193440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$717B561C-8A82-4055-9B6E-8DD9CC9048A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a28056ed53ef07a9d6632c6440711fd2b65f1640","datavalue":{"value":{"entity-type":"item","numeric-id":1159461,"id":"Q1159461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$4FAA799D-1F9D-4238-9C7D-7C4F1AADD795","rank":"normal"},{"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":"Q1124311$3E7BA1E2-0FAA-4519-BAEC-48F80E71D7A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f98fcb838e1ffda9760ba9520630c9b15bdc35b0","datavalue":{"value":{"entity-type":"item","numeric-id":3673097,"id":"Q3673097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$34CFB2B0-EBED-4C2F-834C-4761C56666B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3e396944a512d57143fe2b767f389d5e78258a3","datavalue":{"value":{"entity-type":"item","numeric-id":3719798,"id":"Q3719798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$71BA411A-B65D-4679-9D8B-A2525C4F6FB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d346d8485da0bc889f787fa277d331b616d4df2","datavalue":{"value":{"entity-type":"item","numeric-id":4054648,"id":"Q4054648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$B589473B-A46B-40A7-B270-B1A6B16AD0F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7325afe239c801675ff5fbd404331d1656338d02","datavalue":{"value":{"entity-type":"item","numeric-id":760793,"id":"Q760793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$6EC40B75-EA24-4A8E-A009-13616632CFBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3b21e90a23a5672c558c84dfaa27ce2856c251a","datavalue":{"value":{"entity-type":"item","numeric-id":1162355,"id":"Q1162355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$7101BC67-49D7-4A77-9D87-AE20BA9E24F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7060a8920252488157af075a2c93972723a2ab3","datavalue":{"value":{"entity-type":"item","numeric-id":3769956,"id":"Q3769956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$44168C1F-3673-4D6E-B45E-E33BF1C63F1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1820c23955b4fdf05c16f6b7b19650e00ca1b28","datavalue":{"value":{"entity-type":"item","numeric-id":3960106,"id":"Q3960106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$0316DD1C-6ED0-4982-92E4-E8397760EFC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9178378ae59b37fa519432d09b89f67083d636e5","datavalue":{"value":{"entity-type":"item","numeric-id":1822934,"id":"Q1822934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$18C782D7-3AA3-4493-8AEA-853E7AAA28A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5f83c85c3c55b3dfc7804518e3d46331adb457c","datavalue":{"value":{"entity-type":"item","numeric-id":4726228,"id":"Q4726228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$51E65086-E7C2-4340-84C1-D0C2711F2FE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04423ef643adfc05648864517dad32b25804c149","datavalue":{"value":{"entity-type":"item","numeric-id":3870277,"id":"Q3870277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$2022ED03-9583-4D97-8146-E254C0DEE267","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea1881713e24fbe622e6fb3d2904bb01b3053281","datavalue":{"value":{"entity-type":"item","numeric-id":3029010,"id":"Q3029010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$E0A5BB4A-D30B-446B-8BEC-6EF5E6F43CF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a7a3316329cfce249f69c13171c2ebaf3fd06f7","datavalue":{"value":{"entity-type":"item","numeric-id":3956390,"id":"Q3956390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$81647511-16F8-46AC-8783-B784FF02361E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3ae2b43295e8f75713cc545a37c2780fa87a9c2","datavalue":{"value":{"entity-type":"item","numeric-id":1077159,"id":"Q1077159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$E4A2A6D0-D10A-4CA9-9C7B-3AD7A62B2EFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8e3d5efcad955e9874c3cad0d3e003718384f33","datavalue":{"value":{"entity-type":"item","numeric-id":1143164,"id":"Q1143164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$D3E647C3-76E2-478F-B9AE-096B2E1E9B72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c58698a601ad88e9de7fc1a25166a184d7467e4","datavalue":{"value":{"entity-type":"item","numeric-id":4744268,"id":"Q4744268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$0C885E7C-B7FC-40F5-8C9E-4DEF3D95F1E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72a5ea97f81b547cbf103e27040dc6f1c9a350cb","datavalue":{"value":{"entity-type":"item","numeric-id":580955,"id":"Q580955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$518B8A75-E0FB-4AF0-844B-45F93B694393","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa88669227141db71dbbde7111e0cc29dbacbe07","datavalue":{"value":{"entity-type":"item","numeric-id":801661,"id":"Q801661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$6F7D065B-7F25-4A4C-A24A-366657124CE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"178206957f1ef7c0cd7065687539a80ddab0dcef","datavalue":{"value":{"entity-type":"item","numeric-id":3698302,"id":"Q3698302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$531D8567-429E-493E-9427-CBEF86C13D8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a1fa5d6f6c733523cd9ea7f235a2f6db60ee340","datavalue":{"value":{"entity-type":"item","numeric-id":3956920,"id":"Q3956920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1124311$FCB06692-A47F-4C9C-9B5B-A04132490116","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d2235f5043c5c02ba72156c260d6b677974f5e4","datavalue":{"value":{"entity-type":"item","numeric-id":3698302,"id":"Q3698302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5aaa709786a558da667d12d4506afc5a4581e29e","datavalue":{"value":{"amount":"+0.7661102414131165","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":"Q1124311$BE6B1EAC-4491-45DC-9231-142F017C156C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"562c92cb91f0b2ecd3f6b1b6b8e9d74cd40afb2a","datavalue":{"value":{"entity-type":"item","numeric-id":3012541,"id":"Q3012541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8e285790b4e74ad5eed3c47be17170c77bd4b07","datavalue":{"value":{"amount":"+0.753690779209137","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":"Q1124311$738AF5A4-94E8-4D8F-9553-0F8562F5B9D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ea95e49f05526edb7368d843c6ed27a9c17b632","datavalue":{"value":{"entity-type":"item","numeric-id":4923522,"id":"Q4923522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b61f68c1be638816f5b7d8f40c5cecbffc38b21f","datavalue":{"value":{"amount":"+0.7483245730400085","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":"Q1124311$8E99E1B9-E8F1-47A9-8DB8-ACC176B40146","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7423c6b18bde8ebaa3ad7e0f0ef08b8ee7573835","datavalue":{"value":{"entity-type":"item","numeric-id":3814773,"id":"Q3814773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"af973a27e3c0ad076299b62e2a33f21c0fe84715","datavalue":{"value":{"amount":"+0.7455676794052124","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":"Q1124311$83663C66-763F-4713-982F-97E8AB707ACB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b5021350f22a56a4f8a6bf18c312e072b067944","datavalue":{"value":{"entity-type":"item","numeric-id":3995530,"id":"Q3995530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2fdb4bd03e8cf0e5817918852e2d896bc75c8118","datavalue":{"value":{"amount":"+0.7442164421081543","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":"Q1124311$A47B1E34-F41E-4195-A2ED-AB33E783EB97","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Weak second order characterizations of various program verification systems","badges":[]}}}}}