{"entities":{"Q1091122":{"pageid":1101874,"ns":120,"title":"Item:Q1091122","lastrevid":69620046,"modified":"2026-04-13T08:15:02Z","type":"item","id":"Q1091122","labels":{"en":{"language":"en","value":"A Hoare-like proof system for analysing the computation time of programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4009802"}},"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":"Q1091122$C68E82B9-ABCD-4B49-927D-5E1A0E47DCF1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6197f5bcfa7528dd68ed86816284124338e50aec","datavalue":{"value":{"text":"A Hoare-like proof system for analysing the computation time of programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1091122$832809DF-C9C0-4473-9E5A-F46743BB9C1E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cafd23329b9569b4d3e0fb9c0912dcf1e10d988c","datavalue":{"value":"0622.68026","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091122$722839D1-CCC2-4C23-BF9F-65A7837BEC79","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"209227a6057fd4319571c1ffb8af3fcaac8ee0f8","datavalue":{"value":"10.1016/0167-6423(87)90029-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091122$D1D71423-249D-48AB-B239-C092B6D3E0F2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cf7e7b304afc261de9ac094852ee3a0db52eaac7","datavalue":{"value":{"entity-type":"item","numeric-id":492909,"id":"Q492909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1091122$7B1D0A3F-E38C-4911-B027-69F152AB0BFA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4082512e7d3530b9726df691c7c28e9fec542a8c","datavalue":{"value":{"entity-type":"item","numeric-id":169675,"id":"Q169675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1091122$D00A2ED3-8CF8-4AED-9C2C-DF239F5FC73B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-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":"Q1091122$0E7CCAC6-E3D8-4808-8BEB-C46B2F50A382","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2f41b9d2445ca90f0a280e38510c3e53f90ca911","datavalue":{"value":"Versions of Hoare logic have been introduced to prove partial and total correctness properties of programs. In this paper it is shown how a Hoare-like proof system for while programs may be extended to prove properties of the computation time as well, it should be stressed that the system does not require the programs to be modified by inserting explicit operations upon a clock variable. We generalize the notions of arithmetically sound and complete and show that the proof system satisfies these. Also we derive formal rules corresponding to the informal rules for determining the computation time of while programs. The applicability of the proof system is illustrated by an example, the bubble sorting algorithm.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091122$4373A782-E1CB-46C6-907D-9F8AC134B430","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091122$E82CE454-1EDB-4FA8-AB4F-0594FDB02D2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f97694d44af155a68434cb72eabc6a4d5dd5227","datavalue":{"value":"68P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091122$AA28FB63-5818-4C45-8A74-7B1A0B63917A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9ea0537a570fbc4cf3f775d7f2e67c73cef597a8","datavalue":{"value":"4009802","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091122$73E2E5F7-4929-4DB1-8376-F91398EAB84D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091122$BBAEF39C-1031-4D82-BB1E-6BAFE6B4C079","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b378b3ac878ee58ac594cfc2120dc04a7c6b5e77","datavalue":{"value":"partial and total correctness properties of programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091122$DE1E17AC-20E7-4DF9-9C4B-2530F9EECBA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bcdf35d350cd6ce70941db7b755a152d771d3f8d","datavalue":{"value":"while programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091122$4930AFC0-6C1B-4BF7-915F-5C99D71BC393","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aaea35cb6d40cc89868a51ce9042323e56662ccb","datavalue":{"value":"clock variable","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091122$E9E9A73E-7349-4416-BE9B-E2EC751AEE44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0c4d0a721cf610c5b587ec52bf269f29ba9daf33","datavalue":{"value":"bubble sorting algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091122$9DBB6B22-0B0C-4D8A-97BC-18969524F6EC","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":"Q1091122$E9524E95-F375-4468-B2A2-6164ED62B5E5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3145760d8e18d280da6c45b2cf63f25a29a49915","datavalue":{"value":"https://doi.org/10.1016/0167-6423(87)90029-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q1091122$8B557EEA-D20F-42C2-B147-9716A4E6A675","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"243d605756f9349fd857b21cad6d473772d27524","datavalue":{"value":"W1967175382","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091122$C75CE959-06C3-4EF3-84CA-0F78E110362E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b27080ef660066b784b9e93a914d39f7c1d17460","datavalue":{"value":{"entity-type":"item","numeric-id":3316556,"id":"Q3316556"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b5eedbd760572e2b69440ea82966e96830406285","datavalue":{"value":{"amount":"+0.8762985467910767","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":"Q1091122$1DE9D2B8-ADA3-42E5-B2FF-7FE5097F2DE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5bd8a7822cda824c38b820415ea88d6dc95dcb8f","datavalue":{"value":{"entity-type":"item","numeric-id":2324211,"id":"Q2324211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e2717a16c3bc3a142dc9f56825d5567bd275c8b","datavalue":{"value":{"amount":"+0.8033965229988098","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":"Q1091122$C4B3BA5E-153B-4320-B6B3-4407D67037DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bdb4a09b3436528ff53ecbd19b34ce8215675f75","datavalue":{"value":{"entity-type":"item","numeric-id":3221388,"id":"Q3221388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a09f662863799017fce27d83718cef23415c210e","datavalue":{"value":{"amount":"+0.761685311794281","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":"Q1091122$6D1D5005-ADC3-427C-A541-41E37BE15058","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6fc03231c8b2da69323dec19dd32ea7016e52a15","datavalue":{"value":{"entity-type":"item","numeric-id":3975138,"id":"Q3975138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"432a761a214ade9382fa0f3d01a93b31073414d7","datavalue":{"value":{"amount":"+0.7527397871017456","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":"Q1091122$CB4DF7E0-307A-4E2C-942F-14D35C84ACC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"920a9b4736e3dc9bdd0f1f07e717de567cd54fde","datavalue":{"value":{"entity-type":"item","numeric-id":3678649,"id":"Q3678649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"73792f7e2cf52a9a1fe85361ac733a6fec1a436f","datavalue":{"value":{"amount":"+0.7520688772201538","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":"Q1091122$925834A7-0C30-455B-A390-28BC8DD8BE9E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Hoare-like proof system for analysing the computation time of programs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Hoare-like_proof_system_for_analysing_the_computation_time_of_programs"}}}}}