{"entities":{"Q1111362":{"pageid":1122111,"ns":120,"title":"Item:Q1111362","lastrevid":49223809,"modified":"2026-01-06T19:26:37Z","type":"item","id":"Q1111362","labels":{"en":{"language":"en","value":"A calculus of refinements for program derivations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4076587"}},"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":"Q1111362$644A8F78-F1DB-4357-80C6-CEEB0F606DDB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c7b7b1f4bcf8f8e06bcf908d0522b45d8af341da","datavalue":{"value":{"text":"A calculus of refinements for program derivations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1111362$755C7C64-0369-477F-999B-6D46CD3EA847","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6c7017956183f5f5a4be79d49246b06701dcad98","datavalue":{"value":"0658.68018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1111362$F1829F83-56BE-42D5-93EB-A59FAB9EAD6F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"018cb99c8397272cfe149ec75a886825639231ba","datavalue":{"value":"10.1007/BF00291051","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1111362$91B8F564-6F0D-4015-A080-9E0A3D20796B","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":"Q1111362$030A84D8-A75A-4EC8-8F6A-1B67B70A7AED","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-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":"Q1111362$CF962789-4F74-4794-86F5-1DF5076536CF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e69b40a4f72573e4593f2564af49f0abbff433f4","datavalue":{"value":"This paper presents a semantic formalization of the stepwise refinement programming method. It extends earlier work of the same author, but it is selfexplanatory. The basic notion of the author's refinement calculus is the relation of correct refinement between programs: A program S is said to be correctly refined by another program S' if S' satisfies any specification that S satisfies. Specifications are treated as (non- executable) program statements, which determine a well-defined effect on the program state. Since a specification may be restricted to some of the properties, it acts like a nondeterministic statement.    The approach is based on predicate transformers (Section 2) and is illustrated using a simple programming language (Section 3). In Section 4, the precise definition of a correct refinement is given. Then, the author shows that sequential and conditional composition, iteration and recursion are monotonic with respect to the refinement relation. (In an appendix, the author proves monotonicity in the case of unbounded nondeterminism.)    The main result is a characterization of a correct refinement by reducing it to a specific pre-/\\(post\\)-condition formula that depends only on the statement being refined. Section 7 analyses the special case that the refinement does not introduce new variables. Finally, context-dependent refinements are considered. A small example rounds off this clearly written paper.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1111362$CC1E2AF0-C6C2-4A09-9B7C-12DBA5E607AD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1111362$26F877E9-0B12-476F-93F9-8EB562670D3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1111362$738D9772-D5FC-499A-913A-48CD717BB425","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d8bb9edecb49c61ff658a658c488ca51459a2eb3","datavalue":{"value":"4076587","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1111362$B615B645-716C-4611-A8B5-DE0BF815C3CF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8199d3c167bb7194c1f4325dd8abc9ea993e9d4d","datavalue":{"value":"program development","type":"string"},"datatype":"string"},"type":"statement","id":"Q1111362$FC02B754-AAB2-474D-8514-C8098A66B017","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"322ea768f2b97508db847d80bb51e98a654d6c56","datavalue":{"value":"program transformation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1111362$94EC2D6A-5718-4E7D-A7F6-281BBA7D7B8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f9ac4ef6ef6c5f8856ee80195276e724e0b6225a","datavalue":{"value":"correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1111362$0A36C512-5DD2-4C05-80EF-D426D1384A39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1111362$65B04E0B-49DE-4D03-B444-953BFA030BFB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f7d76bab915fa5b11ba4114aa1f83889a977dcb6","datavalue":{"value":{"entity-type":"item","numeric-id":204599,"id":"Q204599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$99397574-E507-4D0A-A084-81D434280660","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"022fe16d37aa700fea70e7a830c42e0ea8776f70","datavalue":{"value":{"entity-type":"item","numeric-id":685457,"id":"Q685457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$61B36EFE-B00F-4C27-BB35-2C781136BF40","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aadc3562b5d3cd99740f94e9d46e7f210998eaf","datavalue":{"value":{"entity-type":"item","numeric-id":33419,"id":"Q33419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$07D2FB5B-1A5F-4F44-B9BA-FE964B38D69A","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":"Q1111362$ED20429B-7A70-4C47-9DEA-E8231A386082","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2204ee7d30bcfa8fbee857183801f78bafc2ef2","datavalue":{"value":{"entity-type":"item","numeric-id":3763571,"id":"Q3763571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$2C81F16D-A79A-4B95-9FB3-07759549071B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7469a14c6b3d5214a08da9b6d9960375ad8bda98","datavalue":{"value":{"entity-type":"item","numeric-id":3898009,"id":"Q3898009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$33AC460C-C140-4CEE-84B3-AF8EED4CF576","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e707d4bae687b7a2d018b22ef15d22342b7b2c5","datavalue":{"value":{"entity-type":"item","numeric-id":1155605,"id":"Q1155605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$E18FFFDC-D140-4065-B754-E8265E8BB0C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df2976aa90eeca3f6092c5fdf4fa1ff69fee0cd4","datavalue":{"value":{"entity-type":"item","numeric-id":1157144,"id":"Q1157144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$6D6D74A3-7614-4929-BDA0-59FC2DE146A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fb0085fbad97e351502d04a08e987063d6b6b7a","datavalue":{"value":{"entity-type":"item","numeric-id":4184269,"id":"Q4184269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$C923F6E7-D15C-4D2C-B146-FB67EAEF2B81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac63bb951bd0e8a61ad219b7e42777807041f72c","datavalue":{"value":{"entity-type":"item","numeric-id":3783489,"id":"Q3783489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$97DF322A-5738-48C6-9004-A18094700EAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ffb3e26760d87c71a363189dcbfed536d99889b2","datavalue":{"value":{"entity-type":"item","numeric-id":3954796,"id":"Q3954796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$7D7063C4-2145-4F38-AD8A-6186E6B05E87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06ed2d53bc64078e65a41a4770b143a0881e72e8","datavalue":{"value":{"entity-type":"item","numeric-id":3875322,"id":"Q3875322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$7620B74C-7BFD-4ED6-B94B-BC8875A96ED9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c5ae7e408b1d1201c271e00762d47096e39a012","datavalue":{"value":{"entity-type":"item","numeric-id":4111080,"id":"Q4111080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$25B68543-29DC-4185-BFEB-16C541EE0386","rank":"normal"},{"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":"Q1111362$0E964DB9-1CA5-4946-B2FF-20686AB8AEFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7493c00c260f207a238f41e9e5a3d8b8ed81bd7","datavalue":{"value":{"entity-type":"item","numeric-id":1075045,"id":"Q1075045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$EF64D0E2-4E2C-4776-BC03-3248CA056F6A","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":"Q1111362$470EAFB9-E577-4F87-A0FC-42F9F91AD994","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c82ad10c73e928271f482901deda0f097caa8289","datavalue":{"value":{"entity-type":"item","numeric-id":3723675,"id":"Q3723675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$424E5074-BFAF-441D-9606-145BC4D7DC24","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":"Q1111362$B0FD37F4-A9FA-4A7E-99BE-95FEAAB4726E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d50abac9b5648a878af003e7eaa6c6d610ba9983","datavalue":{"value":{"entity-type":"item","numeric-id":5621948,"id":"Q5621948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$FC72E673-4621-497B-BDDE-B3020984A846","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30331b0843d8fad412757315603331be3191b0d9","datavalue":{"value":{"entity-type":"item","numeric-id":4711615,"id":"Q4711615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$5474084D-C169-45EC-9DCF-7216C6197A3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db45f234f354c516e6967660fb11814401792350","datavalue":{"value":{"entity-type":"item","numeric-id":578892,"id":"Q578892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$1B7D412F-DAAC-4F66-B67B-2384DD439848","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f77d0fd94b4ba1a2f231f232c1cf313c408a00a","datavalue":{"value":{"entity-type":"item","numeric-id":2265798,"id":"Q2265798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$78F66E10-24CC-450F-92C6-EDB4B71A3166","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a24bd10a27e1b8e759cf20e25bbc96fc409e8f8","datavalue":{"value":{"entity-type":"item","numeric-id":4127356,"id":"Q4127356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$D4AF7FEE-9A05-46C1-8DD8-C521B370C554","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"340b1a67b2cb88bc1a79812f682d43444abf5b93","datavalue":{"value":{"entity-type":"item","numeric-id":3932278,"id":"Q3932278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$C805B5F2-297C-452C-B315-98F4094918D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07a66aca149d54d7dff0ef6032122ab7db2b935e","datavalue":{"value":{"entity-type":"item","numeric-id":5551146,"id":"Q5551146"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$3606AEB7-1C4D-47EE-90A0-407F6230E627","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9cf91379516875102cbd34cc81bf4325eee6d826","datavalue":{"value":{"entity-type":"item","numeric-id":1251475,"id":"Q1251475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$E584FE12-91EC-4C7A-B0C4-56D56A214D83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78b7dee6e7d17cf76652241ef534151263d94379","datavalue":{"value":{"entity-type":"item","numeric-id":5617313,"id":"Q5617313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1111362$89D82C77-674B-4549-9D12-925DBC16DD2B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b3a2e9ba8320592289adda5aae816196601ecbe4","datavalue":{"value":"https://doi.org/10.1007/bf00291051","type":"string"},"datatype":"url"},"type":"statement","id":"Q1111362$8CF1FA07-7C27-4321-829D-4D6DFB5385F8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"44f511319fa822eede0c87e39843d98e56b13364","datavalue":{"value":"W2038814435","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1111362$360F052C-C8A1-4C97-87B5-3E894D8008BE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad830adf215314f88d85a625d9beab8493dd4c12","datavalue":{"value":{"entity-type":"item","numeric-id":578892,"id":"Q578892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"98a92fca83d278781b9d91dffbac71bdc8cfdb1e","datavalue":{"value":{"amount":"+0.8909565806388855","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":"Q1111362$3B1E6253-F69F-4D51-8AB0-79EAE5419FF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e2d4dcc1960b15b4793a79b80662e02a9401a86","datavalue":{"value":{"entity-type":"item","numeric-id":4396958,"id":"Q4396958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b4ab0b9740fa2f4d76fd42eaafbf20e50c54fd2","datavalue":{"value":{"amount":"+0.8418281078338623","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":"Q1111362$2E36A926-A80E-4FC9-BBA1-A74E23C5FB6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"19e9309691e6dae97032b2f3ec7c3e38decde3b7","datavalue":{"value":{"entity-type":"item","numeric-id":4727399,"id":"Q4727399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e9a586431eeebfa607090270ac0fcd20fec92ad","datavalue":{"value":{"amount":"+0.8418278098106384","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":"Q1111362$F673400E-47A7-4585-BD6B-50A5A20945C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95ac42d60317fde4c37666f10d986c26a4eaeea0","datavalue":{"value":{"entity-type":"item","numeric-id":4452605,"id":"Q4452605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c5b730a67ba6ecebca63b4126c5e7ebcc6b1d146","datavalue":{"value":{"amount":"+0.8343846201896667","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":"Q1111362$2EBFF8B0-CB79-44BF-B00D-C8B04A66872F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fbf40fe6e41abe507700f2b9818bffab569481e9","datavalue":{"value":{"entity-type":"item","numeric-id":4281676,"id":"Q4281676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"557423fef401ab67d0e165b2fc75e9dc388b5fbe","datavalue":{"value":{"amount":"+0.8266693353652954","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":"Q1111362$CEDB5246-B8F0-4F23-8951-1B14478B4E37","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1111362","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1111362"}}}}}