{"entities":{"Q1104730":{"pageid":1115479,"ns":120,"title":"Item:Q1104730","lastrevid":66725751,"modified":"2026-04-12T12:26:07Z","type":"item","id":"Q1104730","labels":{"en":{"language":"en","value":"A sharp proof rule for procedures in WP semantics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4056976"}},"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":"Q1104730$298DF3C0-A410-4F62-932E-7DC1E2742AE1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f20f21eb6d482356918daa5d4005ebaa94e51f50","datavalue":{"value":{"text":"A sharp proof rule for procedures in WP semantics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1104730$E32AB104-2798-45C3-8B1C-338C5A9EE186","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4f502369517952a73ab86c29d1c86d3466dcff29","datavalue":{"value":"0647.68017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1104730$07E8A447-6C05-4EAC-B905-6692DE097790","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6fcfcac1d49a42ee7d6b0100f1666430b9cee40e","datavalue":{"value":"10.1007/BF00289144","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1104730$0DE8CD80-8741-4852-A4F8-80BF578EE06D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"40652b17d4e74c410674384aadc2536d52890102","datavalue":{"value":{"entity-type":"item","numeric-id":685523,"id":"Q685523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1104730$C8D0A3AE-9E93-474C-9AD5-FA3970D5A5D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0bf8b7ff9c3b8bd65cf4d5fc513ea89473570cc8","datavalue":{"value":{"entity-type":"item","numeric-id":1065534,"id":"Q1065534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1104730$8C52091E-8501-4177-B00B-34BF2E421297","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5fe3007875b0023283ff9d52c210545085c1f7e8","datavalue":{"value":{"entity-type":"item","numeric-id":1064047,"id":"Q1064047"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1104730$7149A20B-9602-42D0-ACC9-9E1BA4B61430","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1104730$5842186C-1104-4497-BBFC-5774575CB656","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":"Q1104730$3B81CFB3-B249-4A1D-BC18-8A50495389A0","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"52cc9780e039f6d4acd9771c4e78050a4b835fd8","datavalue":{"value":"We present a proof rule for the procedure call that is sharp; that is, the precondition it defines is the weakest precondition that can be inferred solely from the procedure's specification. Thus the rule enforces exactly the abstraction introduced by the specification.    If the procedure has formal parameters (`value' x, `value result' y, `result' z), and is called with corresponding actuals (a,b,c), then our rule gives a precondition for the call of  \\[  (\\exists m\\cdot U^{x,y}_{a,b}) \\wedge (\\forall y,z\\cdot (\\forall m\\cdot U^{x,y}_{a,b\\quad} \\Rightarrow V\\quad x_ a) \\Rightarrow E^{b,c}_{y,z})  \\]  where U and V are the pre- and postcondition of the procedure, and E is the postcondition of the call.    We give a simple proof of the soundness and sharpness of our rule, and present an example illustrating the non-sharpness of Gries' proof rule.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1104730$94061894-749C-4FE0-ACBB-890817B2018A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1104730$28AECBD1-A036-48DA-8807-04A731FA3473","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1104730$A46A7645-AC8B-4CF3-8BB0-D248640ADB5C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"00956b60175461aceaee431e03953a6ec53612ba","datavalue":{"value":"4056976","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1104730$35BAF9D2-2BDF-4BF6-A40C-900A2BE2E170","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0134d0e80cc66251ea37da23eec5d4f724e390b9","datavalue":{"value":"WP semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1104730$0A8A5859-370B-42D1-89A3-783172E1934C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"edc54e2ee713bf6ef933abe433da86dc03aec7ba","datavalue":{"value":"proof rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1104730$7ABE95AB-3A3A-4EBE-821D-DC8B1DC8F8CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1a32ec6f9df26104fd1a27ca4deac78da51240f1","datavalue":{"value":"procedure call","type":"string"},"datatype":"string"},"type":"statement","id":"Q1104730$5B1C7C5D-4664-4C1C-929B-3CB011AD85CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"26325b97ca9f91dadc7bc17af7514ea7907cb4fa","datavalue":{"value":"weakest precondition","type":"string"},"datatype":"string"},"type":"statement","id":"Q1104730$1A4CCF80-0484-4AEC-9F44-42ED0CF333B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47511de611e7ca7c7f052290389ebfdae4c32892","datavalue":{"value":"specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1104730$F81F79B2-0C09-422B-930A-EEFE57EF4C7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2d8ce56ee8b42110050dbf827609bd4d689ad8ef","datavalue":{"value":"postcondition","type":"string"},"datatype":"string"},"type":"statement","id":"Q1104730$147C5FDD-9485-4837-8406-4B13C3D62739","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c196bc893ad48ce8a85f32e75f88d6da48862c94","datavalue":{"value":"sharpness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1104730$83D95073-CEAF-4E81-A2A6-AB3D31CAD0D5","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":"Q1104730$EFFB5E98-6AA5-41A2-A138-57CE6E1C757E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"67b8a6374b4fc895d89506f759c76e54380f8254","datavalue":{"value":{"entity-type":"item","numeric-id":4144755,"id":"Q4144755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1104730$BDB36741-9498-4F23-BD9F-49712B733B7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e47b8c90d45ee285590b1a168a8503851fe5b134","datavalue":{"value":{"entity-type":"item","numeric-id":3925859,"id":"Q3925859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1104730$F77F4078-3452-44B6-9041-785ACEA56731","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18b7e8541b8bf7dc514993aa6ba095a6f824bbca","datavalue":{"value":{"entity-type":"item","numeric-id":3922131,"id":"Q3922131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1104730$8CAEFF7D-6218-4915-A0A4-F1170B83893D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d5139d06e1fda093aa2f61489155539944b84d7","datavalue":{"value":{"entity-type":"item","numeric-id":3340184,"id":"Q3340184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1104730$4C951A08-43CB-429B-997A-D4B811E32A23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73afd4a8b9c57c125e3b479571ed5c961d82ebe0","datavalue":{"value":{"entity-type":"item","numeric-id":797986,"id":"Q797986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1104730$6EB6E168-1FE9-4D33-A3E9-AECD2217FF4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81f5a1bf73ad7c6b6dc9013f79221f2ece1c6125","datavalue":{"value":{"entity-type":"item","numeric-id":1838825,"id":"Q1838825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1104730$52125E73-9150-457F-A7E0-FAC1DE352245","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a69d63455715dd4ae7ba0c94f635e6fc6c0fb6c9","datavalue":{"value":{"entity-type":"item","numeric-id":685524,"id":"Q685524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82d4559da9c0fd6a483fd313c5f3bf5557d8b411","datavalue":{"value":{"amount":"+0.8425675630569458","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":"Q1104730$A696E0BE-5752-4553-ADE8-05C593BCA22C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07cf766789bd770230e4ccfc7d996aad8f04d818","datavalue":{"value":{"entity-type":"item","numeric-id":797986,"id":"Q797986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8789cd3d90af0c1796bcd7ea9962e9b95abf129","datavalue":{"value":{"amount":"+0.8410590291023254","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":"Q1104730$373D6391-0A91-4E6C-9C92-48C32EE519DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3cc7c1fe5285b4c9c67abab2af9d685953717ee","datavalue":{"value":{"entity-type":"item","numeric-id":1607103,"id":"Q1607103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b9add0f65d5353b0ee8bd5e97227cab9f727984","datavalue":{"value":{"amount":"+0.8044748306274414","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":"Q1104730$41A0A32E-E84C-4441-8508-87BB86439470","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"acaaea0cc3fa6a8d30716da35caf95fad192a27c","datavalue":{"value":{"entity-type":"item","numeric-id":1329196,"id":"Q1329196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30025b6ac8ad3efdfa620f542bb9478e6a1b3b10","datavalue":{"value":{"amount":"+0.7995645999908447","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":"Q1104730$C9CB9B21-328D-4DA3-961B-026DE0700F8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8dda8ff4b37305d49c5279505db4bfb960d46a96","datavalue":{"value":{"entity-type":"item","numeric-id":3221385,"id":"Q3221385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ee910074e4e6f85f6f166f246bbc15fd729b42a9","datavalue":{"value":{"amount":"+0.79513019323349","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":"Q1104730$34E57623-731F-4EC6-BAB8-5D4391B9ED87","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A sharp proof rule for procedures in WP semantics","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_sharp_proof_rule_for_procedures_in_WP_semantics"}}}}}