Abstract
The algebra of functions and relations has been used so successfully in program construction that textbooks have appeared. Despite the importance of predicate transformers in imperative programming, the algebra of transformers has been less explored. To show its promise, we prove results on exponents and recursion on inductive data types, sufficient for carrying out a polytypic derivation that has been given as a substantial example for functions and relations. We also give a data refinement from exponents of specifications to the concrete exponents needed for program semantics.
Chapter PDF
Similar content being viewed by others
Keywords
References
Bird, R. & de Moor, O. (1996) Algebra of Programming. Prentice-Hall.
de Moor, O. (1992) Inductive data types for predicate transformers. Information Processing Letters 43 (3), 113–118.
de Moor, O. (1996) An exercise in polytypic programming: repmin. Typescript, http://www.comlab.ox.ac.uk/oucl/publications/books/algebra/papers/repmin.ps.gz.
Gardiner, P. H., Martin, C. E. & de Moor, O. (1994) An algebraic construction of predicate transformers. Science of Computer Programming 22, 21–44.
Gardiner, P. & Morgan, C. (1991) Data refinement of predicate transformers. Theoretical Computer Science 87, 143–162.
Jansson, P. & Jeuring, J. (1997) PolyP — a polytypic programming language extension. In Proceedings, POPL, ACM Press, pp. 470–82.
Martin, C. (1995) Towards a calculus of predicate transformers. In Proceedings, MFCS, Vol. 969 of Springer LNCS, pp. 489–49.
Möller, B. (1997) Calculating with pointer structures. In IFIP TC2/WG2.1 Working Conference on Algorithmic Languages and Calculi.
Morgan, C. (1994) Programming from Specifications, second edition. Prentice Hall.
Naumann, D. A. (1994a) Predicate transformer semantics of an Oberon-like language. In E.-R. Olderog, ed., Programming Concepts, Methods and Calculi, IFIP Transactions A-56, Elsevier.
Naumann, D. A. (1994b) A recursion theorem for predicate transformers on inductive data types. Information Processing Letters 50, 329–336.
Naumann, D. A. (1995a) Data refinement, call by value, and higher order programs. Formal Aspects of Computing 7, 652–662.
Naumann, D. A. (1995b) Predicate transformers and higher order programs. Theoretical Computer Science 150, 111–159.
Naumann, D. A. (1996) A categorical model for higher order imperative programming. Mathematical Structures in Computer Science. To appear.
Naumann, D. A. (1998) Beyond fun: Order and membership in polytypic imperative programming. In Mathematics of Program Construction.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Naumann, D.A. (1998). Towards Squiggly Refinement Algebra. In: Gries, D., de Roever, WP. (eds) Programming Concepts and Methods PROCOMET ’98. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35358-6_23
Download citation
DOI: https://doi.org/10.1007/978-0-387-35358-6_23
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6299-0
Online ISBN: 978-0-387-35358-6
eBook Packages: Springer Book Archive