{"entities":{"Q541217":{"pageid":542984,"ns":120,"title":"Item:Q541217","lastrevid":62613180,"modified":"2026-04-11T07:16:27Z","type":"item","id":"Q541217","labels":{"en":{"language":"en","value":"Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5904441"}},"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":"Q541217$BE18A2A5-16C9-4485-B2D0-E0CE843E0CCE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"84470fbd83e681de3a9beb6e363b90df8ff6a5a8","datavalue":{"value":{"text":"Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q541217$A6DC2EC9-4C9A-4956-B8EF-F997F0B87206","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dedc6f5369198f7b0188cec7cc60e5e2abbc0794","datavalue":{"value":"1226.68040","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541217$538DDFE7-BB66-45DF-BCA7-6BA8F6211F3C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"161f1155817cedb591ea8c5b07c833bd18272939","datavalue":{"value":{"entity-type":"item","numeric-id":541216,"id":"Q541216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$6A98ACAE-28FD-48CD-A2B7-551CD74CE1B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c722b18062e530983ece38a50cd0cb269a2811aa","datavalue":{"value":{"entity-type":"item","numeric-id":371256,"id":"Q371256"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$7D81EC84-229A-47D0-8BFE-FB5B89BFEABC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fadd7c9edb175c39860a7070bf646e2e9cc896ac","datavalue":{"value":{"entity-type":"item","numeric-id":165871,"id":"Q165871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$9528D5B6-175F-43E1-B7D7-D359D2DEF670","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":"Q541217$0E88A776-DEDC-47C2-83CA-C4206603F61B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c1d636dc02e31c50ff8e96e46630d760ff43fba8","datavalue":{"value":{"time":"+2011-06-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q541217$A08647EB-5B00-4A93-8999-AE17089B2A0B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a3f8584dfd60fdd385744283f4773daf2f800146","datavalue":{"value":"In this paper a predicate transformer semantics is derived from a direct semantics for a program P in a nondeterministic/probabilistic basic imperative programming language, in the case of partial correctness. The direct semantics for P is given by a function from the set S of states to the convex lower powerdomain of valuations on S. The predicate transformer semantics is obtained by establishing an isomorphism between direct semantics and a continuation semantics. But the authors are more interested in defining from this a predicate transformer wlp corresponding to the intuition of ``weakest liberal preexpectation''. They show how wlp of while-loops can be computed as a greatest fixpoint, allowing to reason about the same while-loops in terms of invariants.","type":"string"},"datatype":"string"},"type":"statement","id":"Q541217$1AE6DBF5-76CD-486B-A28D-A9CEB2BFB7F3","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"bd8c91b20d989f47b6d5b40572fa0e13a50d9a56","datavalue":{"value":{"entity-type":"item","numeric-id":234453,"id":"Q234453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$27D937E6-7A52-48D2-BAAE-3C0D011A2180","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541217$023E7153-0E1F-4CDB-AF37-3CDA971A4F72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541217$1BB4DFF4-3340-4889-A4D6-8B562446F9E9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7aa7dd3d8040fc46f14130d7baade7c785414754","datavalue":{"value":"5904441","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541217$1887D5E3-CD8D-4840-AB27-4770DA6BBC11","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51802126f63d5102d578f2858428d5d0f09da73b","datavalue":{"value":"denotational semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q541217$1689A375-2D31-4EDC-A06D-4B4043122F5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"728818d2de29d948f096f35c669fa7265b9147f5","datavalue":{"value":"predicate transformers","type":"string"},"datatype":"string"},"type":"statement","id":"Q541217$EC2E9409-F312-42C1-BE84-A13BDC81D3AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddb02aa772d5ca9ab71841ccc7e5dfbc96f0964f","datavalue":{"value":"weakest liberal precondition","type":"string"},"datatype":"string"},"type":"statement","id":"Q541217$4215CC3F-4E34-481F-9A45-754F8975F092","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2df76c98afb473da4c54b4dae1d17f708a14925","datavalue":{"value":"probabilistic-nondeterministic computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q541217$B76B7007-05D4-4473-84FF-1014069FD41E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"32c7ccefc1f12473be98f4b71fe5db10caf65d96","datavalue":{"value":"Minkowski duality","type":"string"},"datatype":"string"},"type":"statement","id":"Q541217$C17C4144-F76E-45FD-B5F8-21975AC031E4","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":"Q541217$B9D03D95-B23D-4611-B347-B7C6F8993228","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ff9fbbcdf10fe1fd5ffe480033f271d9e090c288","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2010.12.029","type":"string"},"datatype":"url"},"type":"statement","id":"Q541217$747A1F97-9F1C-41B3-AD35-A498136456BE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c62ebc841eb8b7fa15f69e73d0c95b9b10027e07","datavalue":{"value":"W2013333738","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541217$A80590C3-C6CA-4031-B0AB-63222D43A08C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"23eb2407f5476ca1216e796189f27de1b8b868d0","datavalue":{"value":{"entity-type":"item","numeric-id":4813222,"id":"Q4813222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$71EB7922-3599-4A26-8EA4-2665E79050B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9db762cc0f08fb652d186856f54bfcc71614a4e1","datavalue":{"value":{"entity-type":"item","numeric-id":4787439,"id":"Q4787439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$F63E1D74-F81C-4D39-AC7A-126AA89E790C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b15fe46c86d65b948da2460833dc71e09cb9911","datavalue":{"value":{"entity-type":"item","numeric-id":3636909,"id":"Q3636909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$D0A0E80C-71DA-4E5D-AAEA-3983F36C5D6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69496384de3b7aa121e4db7da81e002bfecb1831","datavalue":{"value":{"entity-type":"item","numeric-id":1023294,"id":"Q1023294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$F324F59F-D921-4C9E-B623-4BB9C9347D88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e70a46df6bd961b87332072844cab9b2ec8e762","datavalue":{"value":{"entity-type":"item","numeric-id":5958768,"id":"Q5958768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$003FE669-6825-40E5-B85C-A774E4812388","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c1591307efdcfd25c5361ed6b6bc0d30639a1f8","datavalue":{"value":{"entity-type":"item","numeric-id":4650346,"id":"Q4650346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$477E83F2-2C22-4504-BE43-3E02E60FBC0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2144fe5495fdeccad8e3a872dd20d5cc6bcce44f","datavalue":{"value":{"entity-type":"item","numeric-id":3415205,"id":"Q3415205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$64C2A574-4954-46A6-AB14-F6CE4527D5D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba2c7ca13e70d3e8faf04a058e006d27ce9b92cb","datavalue":{"value":{"entity-type":"item","numeric-id":371259,"id":"Q371259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q541217$F61B979E-97A5-48E5-9AF9-BEB5C91958C8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4bb846a115c25e45ec819c24c12966c26680d4bc","datavalue":{"value":"10.1016/J.TCS.2010.12.029","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q541217$DB44F2AC-3B49-41BA-8088-E0E189723E30","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"961306653d4826e46ebb5f83c3cdfaf590f748da","datavalue":{"value":{"entity-type":"item","numeric-id":1023294,"id":"Q1023294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c9df4c973c6b0dab44fe587f71acabc6d7ff8670","datavalue":{"value":{"amount":"+0.806057333946228","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":"Q541217$01AFB4EA-95C2-4E59-967D-4CFC31E901A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e101652da24a263a8b807117980cb7f3509644aa","datavalue":{"value":{"entity-type":"item","numeric-id":3636909,"id":"Q3636909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f96f75c9824814c4eb3f1a15707434f82a6387ec","datavalue":{"value":{"amount":"+0.7822685837745667","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":"Q541217$DC59DDE2-AB0B-4D3B-A4D0-1C249D763447","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7be9108c8fcfb83f075bfefb84dde5377179e381","datavalue":{"value":{"entity-type":"item","numeric-id":1101439,"id":"Q1101439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f670a1ee0f8a635a9c535fa89e3af88b43e12c22","datavalue":{"value":{"amount":"+0.7811649441719055","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":"Q541217$43C9CE16-8A15-4CA7-9A77-AF17A1A00628","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"55db6001100ac1396139030a36f4624d4e2e4422","datavalue":{"value":{"entity-type":"item","numeric-id":5958768,"id":"Q5958768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e25d2a17825d6b2492f13aa5b1725f3dc672d34","datavalue":{"value":{"amount":"+0.7742773294448853","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":"Q541217$B276364F-1612-4D47-9D48-7B14C54022BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66bdd46ffe3a9cb63dde62f6e717ec872fb044f9","datavalue":{"value":{"entity-type":"item","numeric-id":2722069,"id":"Q2722069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ebdd0abc95583fda290867829bb4cc762b86c1c","datavalue":{"value":{"amount":"+0.7731813788414001","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":"Q541217$2F0F4AD9-764F-4977-B5B9-296721852525","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Relating_direct_and_predicate_transformer_partial_correctness_semantics_for_an_imperative_probabilistic-nondeterministic_language"}}}}}