{"entities":{"Q1091121":{"pageid":1101873,"ns":120,"title":"Item:Q1091121","lastrevid":69620037,"modified":"2026-04-13T08:15:02Z","type":"item","id":"Q1091121","labels":{"en":{"language":"en","value":"The weakest prespecification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4009801"}},"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":"Q1091121$EED87102-1679-4906-AB4A-6801F13E5907","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"45e3788b29dc6a68a7340aa7a7f109ad37916631","datavalue":{"value":{"text":"The weakest prespecification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1091121$0502F8C0-559D-4C39-8CBB-F178AA9E031F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5f033266ffac8c42915a07e67c4ddc43f7eb814a","datavalue":{"value":"0622.68025","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091121$DDF30135-179D-49DA-A961-94F7568F0153","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"febaf52588526e30e17bd4605f83812be5ae4191","datavalue":{"value":"10.1016/0020-0190(87)90106-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091121$97A65511-38E6-41E1-9846-2A02EC44BFCC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8b4b706e0e1892c8640abf317cd4e1ff44c4fa9","datavalue":{"value":{"entity-type":"item","numeric-id":207989,"id":"Q207989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1091121$0E909290-A568-4DC3-819C-66CC6873D9DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6864df6a81eaf3b55e725ae1e843ca021bc92c02","datavalue":{"value":{"entity-type":"item","numeric-id":578899,"id":"Q578899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1091121$BA46F01E-A6E1-4F06-9D64-8B42CACB0128","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":"Q1091121$CC93F652-11DF-41BE-9645-20A95A7B655B","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":"Q1091121$0676627A-FC90-4323-B976-D471488BF6FF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ada39cd1bde266427da9ac8ef2c8bd476e3d63dd","datavalue":{"value":"This paper introduces the concept of the weakest prespecification of program Q with respect to specification R, written \\(Q\\setminus R\\), and explores its basic properties within the framework of the relational calculus. The weakest prespecification serves the same purpose as Dijkstra's weakest precondition, but generalises it in four ways. (1) The specification R describes not only the desired properties of the final values of the variables, but also their desired relationship with the initial values; such specifications are normal in specification languages like VDM and Z. (2) The program Q may be just the specification of a program still to be written. Consequently, the weakest prespecification can assist in splitting a task R into two subtasks Q and \\(Q\\setminus R\\). (3) A partial relation R is taken as the specification of a guarded command, thus guarded commands can be specified and implemented independently, before being collected into a set with if or do. (4) The programming language is extended to include general recursion.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091121$E26A0278-6B11-49AE-A24B-75EF040D5DD3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091121$C91FE96E-C7D4-4313-873E-1EDC111217FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091121$21643556-31D7-4072-9FAF-E29D2AA88A17","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"64b58350090e55a0a17a00a691f0a1517379a4cb","datavalue":{"value":"4009801","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091121$0CAE3A37-B6CE-4555-A45B-BDD3D64E90F5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d37755158a76f36435655e35b413d7df278569b","datavalue":{"value":"weakest prespecification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091121$1883D352-7702-4309-9890-316586E6826D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97cff52f1f8df429852ad8af8776d8a3d505548d","datavalue":{"value":"relational calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091121$397F12C3-D0F5-4A8B-A3C2-986F40458A67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"26325b97ca9f91dadc7bc17af7514ea7907cb4fa","datavalue":{"value":"weakest precondition","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091121$B7B96376-42EC-463D-87DF-03CC9555E010","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ef34a817c7119f010d5311b76c3270a657af8b48","datavalue":{"value":"guarded command","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091121$FB1468F2-1B3B-4B22-8151-85F0F64BA795","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3215a37f2f3e4759778d3eb8b23b9eede7c28f4","datavalue":{"value":"general recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q1091121$DB6D24AC-1674-4881-8332-B9964E1F1A56","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":"Q1091121$D74C03C9-01EF-41D5-8DB6-99692300551F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"535e21b27d95c793031b5ab0b886df24896d4d6d","datavalue":{"value":"https://doi.org/10.1016/0020-0190(87)90106-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q1091121$A82DC8D5-3952-4BAC-BF60-9964C78C71B6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"eb6de5ddf6b7497abccb9a1cdb47ac0f7eb86180","datavalue":{"value":"W2163008980","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1091121$69549EC2-FBA5-4D8B-894C-0F48B70A7BD6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8bb35da37f778c426b2983248ef781d7ae2d0a1","datavalue":{"value":{"entity-type":"item","numeric-id":796289,"id":"Q796289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1091121$E462664A-02A6-42FC-B46F-E7B41C89D055","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1265d63b4599a3fae507d9b15943296bbefa977b","datavalue":{"value":{"entity-type":"item","numeric-id":4066568,"id":"Q4066568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1091121$D4B12FF4-C0F7-45C2-8FB9-C9DB1567640C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18ac860696e668a9ea3bf009a3485e439b6a4bbd","datavalue":{"value":{"entity-type":"item","numeric-id":3859249,"id":"Q3859249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1091121$4F7E03EE-A968-44B1-B1E6-B62FD49A0016","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b88e7fc444b61b2c5fd045c40ec97d8427b63ca8","datavalue":{"value":{"entity-type":"item","numeric-id":3740201,"id":"Q3740201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9000595977498a0a45823d57c77cdcdf3b2dd413","datavalue":{"value":{"amount":"+0.9387862682342528","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":"Q1091121$0AD6F8B8-85C1-436F-9A0A-69855AB42027","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"25b17a4c09cadfc312d1c735800a532722547ea9","datavalue":{"value":{"entity-type":"item","numeric-id":1104780,"id":"Q1104780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b7fe5e376ed823d3c5d018bbef303c9f700b47a3","datavalue":{"value":{"amount":"+0.8381780385971069","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":"Q1091121$46799CDF-1B77-4271-B7A8-A464ABEB4278","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d5bbbbfdaa289780545d529cd2d253d7b9c3a01d","datavalue":{"value":{"entity-type":"item","numeric-id":3763567,"id":"Q3763567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a699c56b1f2b803d41b22a4124b6b31d554b16ad","datavalue":{"value":{"amount":"+0.7998071312904358","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":"Q1091121$62BFB273-F657-4ABB-8BD7-B9F588213A22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"080ce8ed2ff81eed979e6694d95fe0f358c2162f","datavalue":{"value":{"entity-type":"item","numeric-id":3801525,"id":"Q3801525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c17dc12da5458e644e9e1bd274f3264aa07f8c4f","datavalue":{"value":{"amount":"+0.776129961013794","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":"Q1091121$E8980CD2-BFA0-4CF2-94D7-D1B8D6B7488E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e391b0aa8c6dfe5663003fdb3f9604dbe9836802","datavalue":{"value":{"entity-type":"item","numeric-id":3842954,"id":"Q3842954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a640c0e27029d1c3fd827e29ac9a9abcb7b9e105","datavalue":{"value":{"amount":"+0.7668079137802124","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":"Q1091121$AE9AFC94-0791-486A-B299-8A94123E1A22","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The weakest prespecification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_weakest_prespecification"}}}}}