{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:00:14Z","timestamp":1725487214189},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672579"},{"type":"electronic","value":"9783540464327"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46432-8_24","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:22:02Z","timestamp":1184602922000},"page":"359-374","source":"Crossref","is-referenced-by-count":1,"title":["On the Semantics of Refinement Calculi"],"prefix":"10.1007","author":[{"given":"Hongseok","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uday S.","family":"Reddy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,5,19]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"K. Apt and G. Plotkin. A Cook\u2019s tour of countable non-determinism. In 8th ICALP. Springer-Verlag, 1981.","DOI":"10.7146\/dpb.v10i133.18448"},{"issue":"4","key":"24_CR2","doi-asserted-by":"publisher","first-page":"724","DOI":"10.1145\/6490.6494","volume":"33","author":"K. Apt","year":"1986","unstructured":"K. Apt and G. Plotkin. Countable nondeterminism and random assignment. J. ACM, 33(4):724\u2013767, October 1986","journal-title":"J. ACM"},{"key":"24_CR3","unstructured":"R.-J. R. Back. On the correctness of Refinement steps in program development. Report A-1978-4, Department of Computer Science, University of Helsinki, 1978."},{"key":"24_CR4","unstructured":"R.-J. R. Back. On the notion of correct Refinement of programs. Technical report, University of Helsinki, 1979."},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"R.-J. R. Back","year":"1988","unstructured":"R.-J. R. Back. A calculus of Refinements for program derivations. Acta Informatica, 25:593\u2013624, 1988.","journal-title":"Acta Informatica"},{"key":"24_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R.-J. R. Back","year":"1998","unstructured":"R.-J. R. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, Berlin, 1998."},{"key":"24_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/3-540-57182-5_22","volume-title":"Math. Foundations of Comput. Sci.","author":"M. M. Bonsangue","year":"1993","unstructured":"M. M. Bonsangue and J. N. Kok. Isomorphism between state and predicate trans-formers. In Math. Foundations of Comput. Sci., volume 711 of LNCS, pages 301\u2013310. Springer-Verlag, Berlin, 1993."},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"M. M. Bonsangue and J. N. Kok. The weakest precondition calculus: Recursion and duality. Formal Aspects of Computing, 6, 1994.","DOI":"10.1007\/BF01213603"},{"key":"24_CR9","volume-title":"Formal Description of Programming Concepts","author":"J. W. Bakker de","year":"1978","unstructured":"J. W. de Bakker. Recursive programs as predicate transformers. In E. J. Neuhold, editor, Formal Description of Programming Concepts. North-Holland, Amsterdam, 1978."},{"key":"24_CR10","unstructured":"E. Denney. A Theory of Programm Refinement. PhD thesis, Univ. of Edinburgh, 1999."},{"key":"24_CR11","volume-title":"A Discipline of Programming","author":"E. W. Dijkstra","year":"1976","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, 1976."},{"key":"24_CR12","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(94)00211-Z","volume":"150","author":"P. H. B. Gardiner","year":"1995","unstructured":"P. H. B. Gardiner. Algebraic proofs of consistency and completeness. Theoretical Comput. Sci., 150:161\u2013191, 1995.","journal-title":"Theoretical Comput. Sci."},{"key":"24_CR13","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/0167-6423(94)90006-X","volume":"22","author":"P. H. B. Gardiner","year":"1994","unstructured":"P. H. B. Gardiner, C. E. Martin, and O. de Moor. An algebraic construction of predicate transformers. Science of Computer Programming, 22:21\u201344, 1994.","journal-title":"Science of Computer Programming"},{"key":"24_CR14","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(91)90029-2","volume":"87","author":"P. H. B. Gardiner","year":"1991","unstructured":"P. H. B. Gardiner and C. C. Morgan. Data Refinement of predicate transformers. Theoretical Comput. Sci., 87:143\u2013162, 1991. Reprinted in [23].","journal-title":"Theoretical Comput. Sci."},{"key":"24_CR15","unstructured":"C. A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992."},{"key":"24_CR16","volume-title":"The Logic of Programming","author":"E. C. R. Hehner","year":"1984","unstructured":"E. C. R. Hehner. The Logic of Programming. Prentice-Hall, London, 1984."},{"key":"24_CR17","first-page":"21","volume-title":"Information Processing 62: Proceedings of IFIP Congress 1962","author":"J. McCarthy","year":"1963","unstructured":"J. McCarthy. Towards a mathematical science of computation. In C. M. Popplewell, editor, Information Processing 62: Proceedings of IFIP Congress 1962, pages 21\u201328. North-Holland, Amsterdam, 1963."},{"key":"24_CR18","unstructured":"J. C. Mitchell. Foundations of Programming Languages. MIT Press, 1997."},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"C. C. Morgan. The specification statement. ACM Trans. Program. Lang. Syst., 10(3), Jul 1988. Reprinted in [23].","DOI":"10.1145\/44501.44503"},{"key":"24_CR20","unstructured":"C. C. Morgan. The cuppest capjunctive capping, and Galois. In A. W. Roscoe, editor, A Classical Mind: Essays in Honor of C. A. R. Hoare. Prentice-Hall International, 1994."},{"key":"24_CR21","unstructured":"C. C. Morgan. Programming from Specifications, 2nd Edition. Prentice-Hall, 1994."},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"C. C. Morgan and P. H. B. Gardiner. Data Refinement by calculation. Acta Informatica, 27, 1991. Reprinted in [23].","DOI":"10.1007\/BF00277386"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"C. C. Morgan and T. Vickers, editors. On the Refinement Calculus. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4471-3273-8_9"},{"issue":"3","key":"24_CR24","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J. M. Morris","year":"1987","unstructured":"J. M. Morris. The theoretical basis for stepwise Refinement and the programming calculus. Science of Computer Programming, 9(3):287\u2013306, December 1987.","journal-title":"Science of Computer Programming"},{"issue":"4","key":"24_CR25","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1017\/S0960129598002552","volume":"8","author":"D. Naumann","year":"1998","unstructured":"D. Naumann. A categorical model for higher order imperative programming. Math. Struct. Comput. Sci., 8(4):351\u2013399, Aug 1998.","journal-title":"Math. Struct. Comput. Sci."},{"key":"24_CR26","unstructured":"D. Naumann. Predicate transformer semantics of a higher order imperative language with record subtypes. Science of Computer Programming, 1999. To appear."},{"issue":"4","key":"24_CR27","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G. Nelson","year":"1989","unstructured":"G. Nelson. A generalization of Dijkstra\u2019s calculus. ACM Trans. Program. Lang. Syst., 11(4):517\u2013561, October 1989.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"24_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1007\/3-540-10007-5_48","volume-title":"Abstract Software Specifications","author":"G. D. Plotkin","year":"1980","unstructured":"G. D. Plotkin. Dijkstra\u2019s predicate transformers and Smyth\u2019s power domains. In D. Bjorner, editor, Abstract Software Specifications, volume 86 of LNCS, pages 527\u2013553. Springer-Verlag, 1980."},{"key":"24_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1007\/BFb0036946","volume-title":"Intern. Colloq. Aut., Lang. and Program","author":"M. B. Smyth","year":"1983","unstructured":"M. B. Smyth. Powerdomains and predicate transformers: A topological view. In J. Diaz, editor, Intern. Colloq. Aut., Lang. and Program., volume 154 of LNCS, pages 662\u2013675. Springer-Verlag, 1983."},{"key":"24_CR30","unstructured":"J. E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977."},{"issue":"2","key":"24_CR31","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 characterization of weakest preconditions. J. Comput. Syst. Sci., 15(2):209\u2013212, 1977.","journal-title":"J. Comput. Syst. Sci."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46432-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T03:32:01Z","timestamp":1556681521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46432-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672579","9783540464327"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-46432-8_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}