{"entities":{"Q793507":{"pageid":795355,"ns":120,"title":"Item:Q793507","lastrevid":64423524,"modified":"2026-04-11T19:46:26Z","type":"item","id":"Q793507","labels":{"en":{"language":"en","value":"Partial correctness: The term-wise approach"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3856380"}},"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":"Q793507$06AD3B32-80D0-4832-B4B3-B10D6C9A02D0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"43701d75d50242ef39463bb703e8e90eba94bfb5","datavalue":{"value":{"text":"Partial correctness: The term-wise approach","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q793507$34CB85DE-BF45-44A9-AF2E-DA4A3FAC7282","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"164d14b81c2315622777d609626b595dbd5dd83e","datavalue":{"value":"0538.68008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q793507$703E161F-C23E-4FD7-AB9F-178863F82E1F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4f597a4483c2c48ae4095f3bc960debcfb9747c6","datavalue":{"value":"10.1016/0167-6423(84)90017-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q793507$EDEDD65F-B0E7-4FA0-80F1-93606CE17B8E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8c73fcafe26254af46ee329dcb936cacf9353bb6","datavalue":{"value":{"entity-type":"item","numeric-id":229500,"id":"Q229500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q793507$F21954EF-3707-4D24-8469-F88E4E4199FC","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":"Q793507$65F7456A-0997-43E0-AB70-221E8F06B35B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-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":"Q793507$0047FA0E-313F-4947-B1A1-3FB05E71CAEE","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8fbca48aea8c0badd6f1257264ed5f36ec6213cc","datavalue":{"value":"The first reason to consider the correctness of programs with respect to terms rather than predicates is a simple observation that the classical Hoare's logic, although complete, is too weak to specify programs. Even if we know that a command c is correct w.r.t. predicates \\(n\\geq 0\\) and \\(x=n!\\) we still cannot claim that c computes factorials since c might update n instead (e.g. c might be: \\(n:=0\\); \\(x:=1)\\). A way out put forward in the paper is to allow \\(\\{t_ 1\\}c\\{t_ 2\\}\\) where \\(t_ 1\\) and \\(t_ 2\\) are terms, to mean the value of \\(t_ 2\\) after execution of c is, if defined, equal to the value of \\(t_ 1\\) before. Now \\(\\{\\) n!\\(\\}\\) \\(c\\{\\) \\(x\\}\\) means that c assigns to x the factorial of the initial value of n. The actual calculus of the term-wise correctness turns out very close to the classical Hoare's logic with the backward substitution (in terms) and the loop invariants (terms as well). The generalization onto procedures and functions is easier than is the case with the Hoare's logic. The paper gives the inference system which is sound and relatively complete.","type":"string"},"datatype":"string"},"type":"statement","id":"Q793507$DEFF8C23-EDE3-43B3-BBD2-81504FFCC609","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q793507$0C7459BD-8D38-41F9-8F9C-28D1F81BAE2B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5a3f19a65bf6f3e7fa31328baa6e38f0d2cee73a","datavalue":{"value":"3856380","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q793507$B9E929B8-3860-4436-A052-446420DA757E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"35a46bb2cf42faf99daf63a4d28750916e4d3a1b","datavalue":{"value":"term-wise correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q793507$AB4232B3-3F53-4CE0-B884-2E531692209D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"54dc584da34b31b42e45653eeb6db4b5d65ede21","datavalue":{"value":"applicative features","type":"string"},"datatype":"string"},"type":"statement","id":"Q793507$95451C01-514E-40FD-977D-8FA344ED5E22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a6ca3089f4a9c1f132e8f874f7fe0c6338d24ce7","datavalue":{"value":"Hoare's logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q793507$9357C2B0-4349-4BDB-95A2-A7D97FD65DE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe51228e17b836f3520db7bc0de40e5086eebee3","datavalue":{"value":"soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q793507$93902061-D1FC-4423-8A05-C183A85584E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q793507$81EDD9DA-7B7C-4E15-B6EA-57BA01F05BEF","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":"Q793507$F666BD5E-7C36-4B3A-A292-DD830A2B850C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c35df3cee2d8f9b16293898cc8bcfc77060327d6","datavalue":{"value":"https://doi.org/10.1016/0167-6423(84)90017-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q793507$1EC659E2-9A24-474D-8670-B530600F042F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"23277a24e47a136ef41a629ac4d5e7efab29f5e7","datavalue":{"value":"W1963991971","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q793507$A5FAE998-7656-481D-A7C3-152D0E484EC6","rank":"normal"}],"P1643":[{"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":"d2d396216e060024ab7927896c017b836b3ffa56","datavalue":{"value":{"amount":"+0.8072152137756348","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":"Q793507$C209DDC9-7A6C-4010-A95E-D80C9E769B67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"06b4dbc68b06bc8ecd04f5d1802c7e4cf586f269","datavalue":{"value":{"entity-type":"item","numeric-id":1110500,"id":"Q1110500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64bfcad873a2b1372e8c332c144779342f3555b1","datavalue":{"value":{"amount":"+0.7800812721252441","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":"Q793507$EA920BF9-1DB9-46F7-B13F-02CCA3D1EF0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3df2062477e400153324e8a42104b32141a25c9f","datavalue":{"value":{"entity-type":"item","numeric-id":2265798,"id":"Q2265798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8e2062c49787c41b391598078ad3e392858d5f7","datavalue":{"value":{"amount":"+0.7707517147064209","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":"Q793507$66F01E0B-2DB5-405F-B49F-BA3BE679E2DB","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":"9225135bf143c6a0f85ae2997af2a0bae09e24c1","datavalue":{"value":{"amount":"+0.765961229801178","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":"Q793507$7A12F39A-6449-486D-8BB4-9DE6E2767212","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"672d995dd3428eb07ed30b7429a38292a5821170","datavalue":{"value":{"entity-type":"item","numeric-id":3763566,"id":"Q3763566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e7d8bfbe45fc413b1c2bf2e2180626e534f0bc3","datavalue":{"value":{"amount":"+0.7591787576675415","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":"Q793507$868ECE29-F097-4DEE-BAC2-8E7CFCC261A6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Partial correctness: The term-wise approach","badges":[]}}}}}