{"entities":{"Q1177155":{"pageid":1187904,"ns":120,"title":"Item:Q1177155","lastrevid":66768867,"modified":"2026-04-12T12:43:39Z","type":"item","id":"Q1177155","labels":{"en":{"language":"en","value":"Data refinement of predicate transformers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 20012"}},"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":"Q1177155$09F6FCB5-B02B-4564-AFB1-B02B979DD31D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4012f152081f86c851e47ea1587b8441930abceb","datavalue":{"value":{"text":"Data refinement of predicate transformers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1177155$FFCBB6DE-845D-453D-8A1E-5AE602B4860F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f018f306a7872466e64cace513b04fe7a2e0b5eb","datavalue":{"value":"0736.68060","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177155$3E05D1F3-5990-4F21-B489-3CA31718072B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9ead5b7acc7ad217e8656334aee81466d6034986","datavalue":{"value":"10.1016/0304-3975(91)90029-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177155$EDE8ACCE-309F-4B5A-9581-262E98A06387","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cf440a1d97a3d3fa3fa9dbf8f55a722afca85620","datavalue":{"value":{"entity-type":"item","numeric-id":671410,"id":"Q671410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$752DAEDF-CEF7-4100-9286-5B1EF2384927","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd7da412086b8b15808d88fef0b62eb55ea4ac59","datavalue":{"value":{"entity-type":"item","numeric-id":1330444,"id":"Q1330444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$19A54D67-EDB6-4017-95B3-BA40F1BA3222","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$D3F67DF1-419F-471B-9E53-EEA5097AB644","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1422b5e3113eee9dc98f0455d275631058399b8b","datavalue":{"value":{"time":"+1992-06-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1177155$1505EEBE-69EF-409B-BE90-3B5B4DF96C3A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4347ea811a777409be89f5dd24b1962bafe50032","datavalue":{"value":"Data refinement is the systematic substitution of one data type, given in a rather abstract formulation, for another, more concrete one in a program. This transformation, conceived to path the way for a mathematically guided and secure transition from abstract specification to concrete implementation, hinges upon the concept of predicate transformers introduced by Dijkstra. In this theoretical framework the extension of Dijkstra's guarded commands with constructs for specification settles the environment for the kind of data refinement in question. It is developed as a transformation on local blocks of a program and shown to yield an algorithmic refinement of the whole program. Methods for data refinement are presented and abstract data types are at hand to delineate its scope. At least a particular transformer is used to illustrated elaborately data refinement of a simple program.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177155$4D98A63A-05F9-4875-A5C6-BDF74A3EE9D0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177155$73192A55-6A8B-4A22-9A15-B72CF3B3CAC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177155$48DB6647-4509-4DDC-9F10-43B74684B8BF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8f6ca76a014dc5616e0675abca675b5bd26319ec","datavalue":{"value":"20012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177155$4B84F7D3-4C99-4B1A-B887-A9598D0878F2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1657b9e302015499beb20eee5142470398e14a48","datavalue":{"value":"data refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177155$61AE4956-2473-4CC2-A21B-69D18829BF2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"728818d2de29d948f096f35c669fa7265b9147f5","datavalue":{"value":"predicate transformers","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177155$22C99257-FB85-4CB8-A47E-B960CACA9668","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ee7fdf2049db9290d38cc9f0709f4ba151de5a1","datavalue":{"value":"guarded commands","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177155$3F667327-8773-407D-A11A-7DF49047CDFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47511de611e7ca7c7f052290389ebfdae4c32892","datavalue":{"value":"specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177155$F9A9CE3F-D92C-49E1-83DD-14B24E603EC8","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":"Q1177155$F20470FB-F657-4F42-8097-26B83EBB8BB2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9524c4e82bced3694033dce95f7e1c98228b08af","datavalue":{"value":"https://doi.org/10.1016/0304-3975(91)90029-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q1177155$4B45ACC2-CC21-4017-A256-146E6C8BA132","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8eac9e77082544cc8b2fd44258478e0416e36d2c","datavalue":{"value":"W2073708948","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177155$96DEF512-95A4-4A46-9891-941768B234BF","rank":"normal"}],"P223":[{"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":"Q1177155$73785BBA-B330-462A-89F7-731033779366","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":"Q1177155$732F5349-C87C-4F82-8041-9D0BBD16CA12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"226149966044b48001c0682076573b6d91099455","datavalue":{"value":{"entity-type":"item","numeric-id":4773988,"id":"Q4773988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$A15238BA-CEBE-4D5E-83D0-B13EAB1FCF70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db463348657cf41d5ff4d422c54e0c686e6e5dfc","datavalue":{"value":{"entity-type":"item","numeric-id":2554952,"id":"Q2554952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$9EB471B9-9FF8-4133-8ED4-731CB0896913","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5620413217d8e07a62deab92fb58bbd2ca1e9f21","datavalue":{"value":{"entity-type":"item","numeric-id":3740201,"id":"Q3740201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$FC89511E-7F31-4EC7-9FDB-E399F5537BCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d643c9519505ce70f954afc2ea3c543e896e9fb9","datavalue":{"value":{"entity-type":"item","numeric-id":578901,"id":"Q578901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$3B7B010C-05EC-48D4-B7A9-4C3490D969D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa95e3f926378ec692a2f5af0f0675c611c5d525","datavalue":{"value":{"entity-type":"item","numeric-id":3729999,"id":"Q3729999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$EAA51E01-C370-4796-8920-51CEF8B075C4","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":"Q1177155$E640ABDD-8B75-402F-9BA7-BEDF07F35915","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"679987962fb6a664522be0387a84c9c333be2d73","datavalue":{"value":{"entity-type":"item","numeric-id":3766811,"id":"Q3766811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$577D63DE-88CA-421A-AC9D-4E382D89530C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"012b92d370d97f0cd4ff2cdadd43bc8000a781f0","datavalue":{"value":{"entity-type":"item","numeric-id":1114384,"id":"Q1114384"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$0292C732-09D5-470C-8668-FF67DDAB20B3","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":"Q1177155$3660B628-4CED-409E-9076-5E75DF053977","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc9dcf97f1324642e65a88c0357ad0c7fec47b09","datavalue":{"value":{"entity-type":"item","numeric-id":1113664,"id":"Q1113664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177155$9098D1A7-5C96-428F-96D0-059729499C7E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00a0d47d9cd3dd94a04fa364cc9a84f4776fdd31","datavalue":{"value":{"entity-type":"item","numeric-id":913482,"id":"Q913482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6dbee279b598a0f169acf1ea3372074633add9df","datavalue":{"value":{"amount":"+0.799950122833252","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":"Q1177155$B65E5E58-BFFF-4C68-843E-8B49FE7EFC0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c9b923ffdf0d9c2364931d8dbe2f3e66c99a191","datavalue":{"value":{"entity-type":"item","numeric-id":684396,"id":"Q684396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a350d7c29e26c2721d51d35a79a8d39116f80d8","datavalue":{"value":{"amount":"+0.7770471572875977","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":"Q1177155$D596D027-BEA8-4D9E-8ABF-82A010B835BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d03a389a585267318fd7b7efea6a34800fc7f1db","datavalue":{"value":{"entity-type":"item","numeric-id":4250656,"id":"Q4250656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3bf2301603a4008d9cdc9a37858f1e04a0661f1d","datavalue":{"value":{"amount":"+0.7532830238342285","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":"Q1177155$5106A175-5AB8-45A7-9E37-0D893F5FBE60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80a33e26332b680c1eb6b536624ccd81e0fa5c00","datavalue":{"value":{"entity-type":"item","numeric-id":578901,"id":"Q578901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0c95a170ea3e33944c21d194ff43b875ed1ef24","datavalue":{"value":{"amount":"+0.7498227953910828","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":"Q1177155$0AAFDF0A-1D16-4805-9B8C-8219E76AA1B6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Data refinement of predicate transformers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Data_refinement_of_predicate_transformers"}}}}}