{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:43Z","timestamp":1751660503742},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540565963"},{"type":"electronic","value":"9783540475958"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56596-5_30","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:18:30Z","timestamp":1330255110000},"page":"91-109","source":"Crossref","is-referenced-by-count":3,"title":["Semantics, orderings and recursion in the weakest precondition calculus"],"prefix":"10.1007","author":[{"given":"Marcello","family":"Bonsangue","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost N.","family":"Kok","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1006\/inco.1991.9999","volume":"92","author":"S. Abramsky","year":"1991","unstructured":"S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161\u2013218, 1991.","journal-title":"Information and Computation"},{"issue":"4","key":"5_CR2","doi-asserted-by":"crossref","first-page":"724","DOI":"10.1145\/6490.6494","volume":"33","author":"K. R. Apt","year":"1986","unstructured":"K. R. Apt and G. Plotkin. Countable nondeterminism and random assignment. Journal of the ACM, 33(4):724\u2013767, October 1986.","journal-title":"Journal of the ACM"},{"unstructured":"R.-J.R. Back. On the correctness of Refinement Steps in Program Development. PhD thesis, Department of Computer Science, University of Helsinki, 1978. Report A-1978-4.","key":"5_CR3"},{"key":"5_CR4","volume-title":"volume 131 of Mathematical Centre Tracts","author":"R.-J.R. Back","year":"1980","unstructured":"R.-J.R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Centre Tracts. Mathematical Centre, Amsterdam, 1980."},{"unstructured":"R.-J.R. Back. 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, number 430 in Lecture Notes in Computer Science, pages 67\u201393, 1990.","key":"5_CR5"},{"unstructured":"J. W. de Bakker. Mathematical Theory of Program Corretness. Prentice-Hall, 1980.","key":"5_CR6"},{"key":"5_CR7","first-page":"431","volume-title":"Proc. of the IFIP Working Conference on on Formal Description of Programming Concepts-II","author":"E. Best","year":"1983","unstructured":"E. Best. 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, pages 431\u2013452, Garmisch-Partenkirchen, FRG, 1983. North-Holland Publishing Company."},{"key":"5_CR8","volume-title":"Technical report","author":"M. M. Bonsangue","year":"1992","unstructured":"M. M. Bonsangue and J. N. Kok. Semantics, orderings and recursion in the weakest precondition calculus. Technical report, Centre for Mathematics and Computer Science, Amsterdam, 1992. To appear."},{"unstructured":"R.-J.R. Back and J. von Wright. 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, number 430 in Lecture Notes in Computer Science, pages 42\u201366, 1990.","key":"5_CR9"},{"unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.","key":"5_CR10"},{"key":"5_CR11","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00276020","volume":"26","author":"W.H. Hesselink","year":"1989","unstructured":"W.H. Hesselink. Predicate transformer semantics of general recursion. Acta Informatica, 26:309\u2013332, 1989.","journal-title":"Acta Informatica"},{"unstructured":"P. Hitchcock and D. Park. Induction rules and termination proofs. In International Conference on Automata, Languages and Programming, 1972.","key":"5_CR12"},{"key":"5_CR13","first-page":"108","volume-title":"volume 74 of Lecture Notes in Computer Science","author":"M. Hennessy","year":"1979","unstructured":"M. Hennessy and G. D. Plotkin. Full abstraction for a simple parallel programming language. In J. Becvar, editor, Proc. 8th Int'l Symp. on Mathematical Foundations on Computer Science, volume 74 of Lecture Notes in Computer Science, pages 108\u2013120. Springer-Verlag, Berlin, 1979."},{"issue":"2","key":"5_CR14","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1145\/322123.322134","volume":"26","author":"G. Milne","year":"1979","unstructured":"G. Milne and R. Milner. Concurrent processes and their syntax. J. ACM, 26, 2:302\u2013321, 1979.","journal-title":"J. ACM"},{"key":"5_CR15","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J. Morris","year":"1987","unstructured":"J. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"unstructured":"C.C. Morgan, K.A. Robinson, and P.H.B. Gardiner. On the refinement calculus. Technical Report PRG-70, Programming Research Group, 1988.","key":"5_CR16"},{"unstructured":"G. Nelson. A generalization of Dijkstra's calculus. Technical Report 16, Digital Systems Research Center, 1987.","key":"5_CR17"},{"key":"5_CR18","first-page":"527","volume-title":"volume 86 of Lecture Notes in Computer Science","author":"G. D. Plotkin","year":"1979","unstructured":"G. D. Plotkin. Dijkstra's predicate transformer and Smyth's powerdomain. In Proceedings of the Winter School on Abstract Software Specification, volume 86 of Lecture Notes in Computer Science, pages 527\u2013553. Springer-Verlag, Berlin, 1979."},{"unstructured":"G.D. Plotkin. Post-graduate lecture notes in advanced domain theory (incorporating the \u201cPisa Notes\u201d). Department of Computer Science, Univ. of Edinburgh, 1981.","key":"5_CR19"},{"issue":"1","key":"5_CR20","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0022-0000(78)90048-X","volume":"16","author":"M.B. Smyth","year":"1978","unstructured":"M.B. Smyth. Power domains. J. Comput. Syst. Sci., 16, 1:23\u201336, 1978.","journal-title":"J. Comput. Syst. Sci."},{"key":"5_CR21","first-page":"662","volume-title":"Volume 154 of Lecture Notes in Computer Science","author":"M.B. Smyth","year":"1983","unstructured":"M.B. Smyth. Power domains and predicate transformers: A topological view. In Proceeding of ICALP '83 (Barcelona), Volume 154 of Lecture Notes in Computer Science, pages 662\u2013675. Springer-Verlag, Berlin, 1983."},{"key":"5_CR22","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/S0022-0000(77)80006-8","volume":"15","author":"M. Wand","year":"1977","unstructured":"M. Wand. A characterisation of weakest preconditions. J. Comput. Syst. Sci., 15:209\u2013212, 1977.","journal-title":"J. Comput. Syst. Sci."}],"container-title":["Lecture Notes in Computer Science","Semantics: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56596-5_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T14:51:51Z","timestamp":1713624711000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56596-5_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540565963","9783540475958"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-56596-5_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}