{"entities":{"Q1097683":{"pageid":1108435,"ns":120,"title":"Item:Q1097683","lastrevid":69635049,"modified":"2026-04-13T08:21:21Z","type":"item","id":"Q1097683","labels":{"en":{"language":"en","value":"A decomposition rule for the Hoare logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4035105"}},"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":"Q1097683$4FDA2CE1-CB7B-424B-B542-622051BCF7B1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7b9dbf9da76c9c5dccf9f32fa6b5d545cc87d1da","datavalue":{"value":{"text":"A decomposition rule for the Hoare logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1097683$C7E6F685-43A5-4CA1-99C7-D039C244BF85","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7cf452d83d008f3830440d595cfb082ac787fd81","datavalue":{"value":"0635.68004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097683$171343F5-4133-48BC-9FA3-2D8CAF03C422","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4207dc8ceeefa7610a00241564012c075b51789b","datavalue":{"value":"10.1016/0020-0190(87)90006-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097683$38F6D004-D8CE-4860-A23D-24C3CAF04EE3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fbd8d347166af77436aa4bae89e2c3259d9425c5","datavalue":{"value":{"entity-type":"item","numeric-id":350722,"id":"Q350722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1097683$C6DD90CB-C0FF-4382-9F24-ABAD3A57893D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"52fa7d44b58d0511cb8993765bd916aef86052d8","datavalue":{"value":{"entity-type":"item","numeric-id":63092,"id":"Q63092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1097683$CC4FBB22-8340-4F46-8FFA-766D07D6616B","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":"Q1097683$3F86DB93-E17B-41BB-BA35-AFA9B2B3F3F7","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8ec5ace766295763d298e4642703f3ae515f0b0d","datavalue":{"value":"The complexity of program verification by the Hoare logic grows rapidly as the length of the program to be proved increases. This paper presents a mechanism, called a decomposition rule, which reduces the complexity of theorem proving in the program verification. The rule is simple and easy to use when the precondition for the program can be decomposed into several conditions.    The meaning of the Hoare triple \\(\\{\\) \\(P\\}\\) \\(S\\{\\) \\(Q\\}\\) is that if P is true before program S, then Q is true after S is executed provided that S terminates. We can derive the following shift rule, provided that Q is not affected by executing S,  \\[  \\frac{\\{P\\wedge Q\\}S\\{R\\}}{\\{P\\}S\\{Q\\supset R\\}}.  \\]  From this rule, we can derive the decomposition rule,  \\[  \\frac{\\{P\\wedge P_ 1\\}S\\{Q_ 1\\},\\quad \\{P\\wedge P_ 2\\}S\\{Q_ 2\\}}{\\{P\\}S\\{(P_ 1\\supset Q_ 1)\\wedge (P_ 2\\supset Q_ 2)\\}}  \\]  provided that neither of \\(P_ 1\\) and \\(P_ 2\\) is affected by S. The meaning of this rule is that by decomposing the verification into two parts of \\(\\{P\\wedge P_ 1\\}S\\{Q_ 1\\}\\) and \\(\\{P\\wedge P_ 2\\}S\\{Q_ 2\\}\\), we can have a rather complicated postcondition \\((P_ 1\\supset Q_ 1)\\wedge (P_ 2\\supset Q_ 2)\\). An illustrative example of program by this rule is given.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1097683$827513E6-6801-43E2-B61F-498CC35CC418","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097683$28FA077A-0F4C-412C-899A-E09592561B42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097683$F0568F3E-AFCA-4314-A10D-2CDCB724E22D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"392501cf45cfdd52763b6a848cbc04413ef8aaf1","datavalue":{"value":"4035105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097683$15DAB843-7823-468D-B9C4-A153AC96219A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1097683$05F6D6AC-EB45-4468-B67B-5AF3F95B149C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1097683$092401FA-032F-45E1-86BF-C367F8B2021B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"567410726faac46e1473f1dc376ad52b51cb31a1","datavalue":{"value":"decomposition rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1097683$62FF6D79-867C-4D6C-B340-7126B9212867","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"606b83355235a83c393360f2928788d9941f7846","datavalue":{"value":"complexity of theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1097683$421DFF31-312D-4D1A-B07F-35175CE5D620","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":"Q1097683$3272DB28-DD01-40C7-B8C5-29BE7D0BC81F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4ca1adc32ccfad6a5702f5403a7170a3d7b60ab0","datavalue":{"value":"https://doi.org/10.1016/0020-0190(87)90006-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q1097683$518E6BE6-DC58-48BA-8738-E2F557DA6E37","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e1ad35f8973b95c7f038aa49fd776071d6a6137b","datavalue":{"value":"W2028808675","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097683$CB58E3F2-9693-466F-AABF-B3BE374991DE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c05a5274ff4e0cdb3e6ef34d413a7f16f96d3b7","datavalue":{"value":{"entity-type":"item","numeric-id":4174692,"id":"Q4174692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1097683$B3678352-89E1-4CF9-AD84-A71F3D38B06B","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":"Q1097683$92F722E5-58DF-4D80-A368-EB107F87BFFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f28430ed9b4f7a26aeb0f032922db74966365595","datavalue":{"value":{"entity-type":"item","numeric-id":1843170,"id":"Q1843170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1097683$481771C6-100C-4E00-B45D-30B335649C11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d83e0d809c9946be35cf8127887d0a3709fa8a8","datavalue":{"value":{"entity-type":"item","numeric-id":4124273,"id":"Q4124273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1097683$B2ED9885-F7C3-4075-A6AD-058856C5E4C3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce3104f3067ca70e9cabc898d9342485c14466d8","datavalue":{"value":{"entity-type":"item","numeric-id":4823140,"id":"Q4823140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"337ac608fb956f57067d8ff70de9900e561dfc8d","datavalue":{"value":{"amount":"+0.7583209276199341","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":"Q1097683$584AC471-C630-42C1-988F-5E7EC14AEF90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30ca2c09a307dad10dc9a230dcf44e6e46d1b443","datavalue":{"value":{"entity-type":"item","numeric-id":855274,"id":"Q855274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eda3c447e4282787fd188a67b62ea90940ab36e3","datavalue":{"value":{"amount":"+0.7578288316726685","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":"Q1097683$10016660-DFCE-4D41-9F83-DCCB2E545632","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d5d164d0a00a459a829f9e8678e23bb39e193c8b","datavalue":{"value":{"entity-type":"item","numeric-id":3163399,"id":"Q3163399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f5aa8c3070e445134f8fe7d33b4df425edeb47d","datavalue":{"value":{"amount":"+0.7464607954025269","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":"Q1097683$4DF989D9-75D1-47F6-AAE0-F1A622FBA631","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":"6fd7039c2305b6301430df33b1d2a1a5abbddbf1","datavalue":{"value":{"amount":"+0.7382079362869263","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":"Q1097683$F63C2C8A-322D-47C5-8543-9DF9FF90C2FF","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":"1b43eb854a345399c2bb9afe234dfbc4f1383408","datavalue":{"value":{"amount":"+0.7350120544433594","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":"Q1097683$41723429-633D-481F-9999-9B7E1007CF0C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A decomposition rule for the Hoare logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_decomposition_rule_for_the_Hoare_logic"}}}}}