{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T13:57:08Z","timestamp":1723471028318},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"Suppl 1","license":[{"start":{"date-parts":[[1994,11,1]],"date-time":"1994-11-01T00:00:00Z","timestamp":783648000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1994,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>An extension of Dijkstra's guarded command language is studied, including unbounded demonic choice and a backtrack operator. We consider three orderings on this language: a refinement ordering defined by Back, a new deadlock ordering, and an approximation ordering of Nelson. The deadlock ordering is in between the two other orderings. All operators are monotonic in Nelson's ordering, but backtracking is not monotonic in Back's ordering and sequential composition is not monotonic for the deadlock ordering. At first sight recursion can only be added using Nelson's ordering. We show that, under certain circumstances, least fixed points for non-monotonic functions can be obtained by iteration from the least element. This permits the addition of recursion even using Back's ordering or the deadlock ordering in a fully compositional way. In order to give a semantic characterization of the three orderings that relates initial states to possible outcomes of the computation, the relation between predicate transformers and discrete power domains is studied. We consider (two versions of) the Smyth power domain and the Egli-Milner power domain.<\/jats:p>","DOI":"10.1007\/bf01213603","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T14:32:57Z","timestamp":1109341977000},"page":"788-800","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["The weakest precondition calculus: Recursion and duality"],"prefix":"10.1145","volume":"6","author":[{"given":"Marcello M.","family":"Bonsangue","sequence":"first","affiliation":[{"name":"Department of Computer Science, Vrije Universiteit, De Boelelaan 1081a, 1081, HV Amsterdam, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost N.","family":"Kok","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Utrecht University, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","volume-title":"Proc. 8th ICALP","author":"Apt K.R.","year":"1981"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_2_1_2_3_2","unstructured":"Back R.-J.R.: On the Correctness of Refinement Steps in Program Development . PhD thesis Department of Computer Science University of Helsinki 1978. Report A-1978-4."},{"key":"e_1_2_1_2_4_2","volume-title":"Mathematical Centre Tracts vol. 131","author":"Back R.-J.R.","year":"1980"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","article-title":"On Correct Refinement of Programs","volume":"23","author":"Back R.-J.R.","year":"1981","journal-title":"Journal of Computer and System Sciences"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Back R.-J.R.: Refinement Calculus part II: Parallel and Reactive Programs. In J.W. de Bakker W.-P. de Roever and G. Rozenberg editors Stepwise Refinement of Distributed Systems: Models Formalisms Correctness Lecture Notes in Computer Science 430 pp. 67\u201393. Springer-Verlag 1990.","DOI":"10.1007\/3-540-52559-9_61"},{"key":"e_1_2_1_2_7_2","unstructured":"de Bakker J.W.: Mathematical Theory of Program Correctness . Prentice-Hall 1980."},{"key":"e_1_2_1_2_8_2","unstructured":"Best E.: Relational Semantic of Concurrent Programs (with some Applications). In D. Bjorner editor Proc. of the IFIP Working Conference on on Formal Description of Programming Concepts-II pp. 431\u2013452 Garmisch-Partenkirchen FRG 1983. North-Holland Publishing Company."},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bonsangue M.M. and Kok J.N.: Isomorphisms between State and Predicate Transformers. In A.M. Borzyszkowski and S. Sokolowoski editors Proc. MFCS '93 Gdansk Poland Lecture Notes in Computer Science 711 pp. 301\u2013310. Springer-Verlag 1993.","DOI":"10.1007\/3-540-57182-5_22"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/BF01213603","article-title":"The Weakest Precondition Calculus: Recursion and Duality","volume":"6","author":"Bonsangue M.M.","year":"1994","journal-title":"Formal Aspects of Computing"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Back R.-J.R. and von Wright J.: Refinement Calculus part I: Sequential Nondeterministic Programs. In J.W. de Bakker W.-P. de Roever and G. Rozenberg editors Stepwise Refinement of Distributed Systems: Models Formalisms Correctness Lecture Notes in Computer Science 430 pp. 42\u201366. Springer-Verlag 1990.","DOI":"10.1007\/3-540-52559-9_60"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","first-page":"l","DOI":"10.1007\/BF00268074","article-title":"A Simple Fixpoint Argument without the Restriction to Continuity","volume":"23","author":"Dijkstra E.W.","year":"1986","journal-title":"Acta Informatica"},{"key":"e_1_2_1_2_13_2","unstructured":"Dijkstra E.W.: A Discipline of Programming . Prentice-Hall 1976."},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/77545"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289091"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/69304.69306"},{"key":"e_1_2_1_2_17_2","volume-title":"Proc. 1st ICALP, Rocquencourt","author":"Hitchcock P.","year":"1972"},{"key":"e_1_2_1_2_18_2","volume-title":"PhD thesis","author":"Meyer J.-J.Ch","year":"1985"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_2_1_2_20_2","unstructured":"Morgan C.C. Robinson K.A. and Gardiner P.H.B.: On the Refinement Calculus. Technical Report PRG-70 Programming Research Group 1988."},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69559"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Plotkin G.D.: Dijkstra's Predicate Transformer and Smyth's Powerdomain. In Proc. of the Winter School on Abstract Software Specification Lecture Notes in Computer Science 86 pp. 527\u2013553. Springer-Verlag 1979.","DOI":"10.1007\/3-540-10007-5_48"},{"key":"e_1_2_1_2_23_2","unstructured":"Plotkin G.D.: Post-Graduate Lecture Notes in Advanced Domain Theory (incorporating the \u201cPisa Notes\u201d). Department of Computer Science Univ. of Edinburgh 1981."},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"de Roever W.P.: Dijkstra's Predicate Transformer Non-Determinism Recursion and Terminations. In Proc. 5th MFCS Lecture Notes in Computer Science 45 pp. 472\u2013481. Springer-Verlag 1976.","DOI":"10.1007\/3-540-07854-1_217"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90048-X"},{"key":"e_1_2_1_2_26_2","first-page":"662","volume-title":"Proc. 10th ICALP","author":"Smyth M.B.","year":"1983"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(77)80006-8"},{"key":"e_1_2_1_2_28_2","unstructured":"von Wright J.: A Lattice-theoretical Basis for Program Refinement. PhD thesis Abo Akademi 1990."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01213603.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01213603\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01213603","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:29:03Z","timestamp":1641482943000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01213603"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,11]]},"references-count":28,"journal-issue":{"issue":"Suppl 1","published-print":{"date-parts":[[1994,11]]}},"alternative-id":["10.1007\/BF01213603"],"URL":"https:\/\/doi.org\/10.1007\/bf01213603","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,11]]}}}