Abstract
Refinement calculi for imperative programs provide an integrated framework for programs and specifications and allow one to develop programs from specifications in a systematic fashion. The semantics of these calculi has traditionally been defined in terms of predicate transformers and poses several challenges in defining a state transformer semantics in the denotational style. We define a novel semantics in terms of sets of state transformers and prove it to be isomorphic to positively multiplicative predicate transformers. This semantics disagrees with the traditional semantics in some places and the consequences of the disagreement are analyzed.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
K. Apt and G. Plotkin. A Cook’s tour of countable non-determinism. In 8th ICALP. Springer-Verlag, 1981.
K. Apt and G. Plotkin. Countable nondeterminism and random assignment. J. ACM, 33(4):724–767, October 1986
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.
R.-J. R. Back. On the notion of correct Refinement of programs. Technical report, University of Helsinki, 1979.
R.-J. R. Back. A calculus of Refinements for program derivations. Acta Informatica, 25:593–624, 1988.
R.-J. R. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, Berlin, 1998.
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–310. Springer-Verlag, Berlin, 1993.
M. M. Bonsangue and J. N. Kok. The weakest precondition calculus: Recursion and duality. Formal Aspects of Computing, 6, 1994.
J. W. de Bakker. Recursive programs as predicate transformers. In E. J. Neuhold, editor, Formal Description of Programming Concepts. North-Holland, Amsterdam, 1978.
E. Denney. A Theory of Programm Refinement. PhD thesis, Univ. of Edinburgh, 1999.
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, 1976.
P. H. B. Gardiner. Algebraic proofs of consistency and completeness. Theoretical Comput. Sci., 150:161–191, 1995.
P. H. B. Gardiner, C. E. Martin, and O. de Moor. An algebraic construction of predicate transformers. Science of Computer Programming, 22:21–44, 1994.
P. H. B. Gardiner and C. C. Morgan. Data Refinement of predicate transformers. Theoretical Comput. Sci., 87:143–162, 1991. Reprinted in [23].
C. A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992.
E. C. R. Hehner. The Logic of Programming. Prentice-Hall, London, 1984.
J. McCarthy. Towards a mathematical science of computation. In C. M. Popplewell, editor, Information Processing 62: Proceedings of IFIP Congress 1962, pages 21–28. North-Holland, Amsterdam, 1963.
J. C. Mitchell. Foundations of Programming Languages. MIT Press, 1997.
C. C. Morgan. The specification statement. ACM Trans. Program. Lang. Syst., 10(3), Jul 1988. Reprinted in [23].
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.
C. C. Morgan. Programming from Specifications, 2nd Edition. Prentice-Hall, 1994.
C. C. Morgan and P. H. B. Gardiner. Data Refinement by calculation. Acta Informatica, 27, 1991. Reprinted in [23].
C. C. Morgan and T. Vickers, editors. On the Refinement Calculus. Springer-Verlag, 1992.
J. M. Morris. The theoretical basis for stepwise Refinement and the programming calculus. Science of Computer Programming, 9(3):287–306, December 1987.
D. Naumann. A categorical model for higher order imperative programming. Math. Struct. Comput. Sci., 8(4):351–399, Aug 1998.
D. Naumann. Predicate transformer semantics of a higher order imperative language with record subtypes. Science of Computer Programming, 1999. To appear.
G. Nelson. A generalization of Dijkstra’s calculus. ACM Trans. Program. Lang. Syst., 11(4):517–561, October 1989.
G. D. Plotkin. Dijkstra’s predicate transformers and Smyth’s power domains. In D. Bjorner, editor, Abstract Software Specifications, volume 86 of LNCS, pages 527–553. Springer-Verlag, 1980.
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–675. Springer-Verlag, 1983.
J. E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977.
M. Wand. A characterization of weakest preconditions. J. Comput. Syst. Sci., 15(2):209–212, 1977.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yang, H., Reddy, U.S. (2000). On the Semantics of Refinement Calculi. In: Tiuryn, J. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2000. Lecture Notes in Computer Science, vol 1784. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46432-8_24
Download citation
DOI: https://doi.org/10.1007/3-540-46432-8_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67257-9
Online ISBN: 978-3-540-46432-7
eBook Packages: Springer Book Archive