Towards a calculus of predicate transformers

  • Clare Martin
Contributed Papers Semantics
Part of the Lecture Notes in Computer Science book series (LNCS, volume 969)


The main purpose of this paper is to investigate whether the relationship between the categories of total functions, relations and predicate transformers described in [7] can be used to develop a calculus of predicate transformers for program derivation in the style of [13] directly from the well established calculus of functions [2]. The results are mixed in the sense that although many laws of the functional calculus can be generalised to predicate transformers, they must be weakened in order to do so.


Functional Calculus Total Function Product Functor Predicate Transformer Program Refinement 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Backhouse, P.J. de Bruin, G. Malcolm, E. Voermans, J. avn der Woude A Relational Theory of Datatypes, in Proceedings of Workshop on Constructive Algorithmics: The Role of Relations in Program Development (1990)Google Scholar
  2. 2.
    R.S. Bird Lectures on Constructive Functional Programming. Technical Monograph PRG-69.Google Scholar
  3. 3.
    R.S. Bird and O. de Moor Solving Optimisation Problems with Catamorphisms. Springer-Verlag Lecture Notes in Computer Science 669 (1992) 45–66.Google Scholar
  4. 4.
    R.S. Bird and O. de Moor Relational Program Derivation and Context-free Language Recognition In: A Classical Mind. Essays in Honour of C.A.R. Hoare. Prentice-Hall (1994) 17–36.Google Scholar
  5. 5.
    A. Carboni, M. Kelly and R. Wood A 2-Categorical Approach to Geometric Morphisms I. Sydney Pure Mathematics Research Reports 89-19 (1989), Department of Pure Mathematics, University of Sydney, NSW 2006, Australia.Google Scholar
  6. 6.
    P.J. Freyd and A. Scedrov Categories, Allegories. North Holland Mathematical Library (1989).Google Scholar
  7. 7.
    P. Gardiner, C.E. Martin and O. de Moor An Algebraic Construction of Predicate Transformers. Science of Computer Programming 22: 21–44 (1994)Google Scholar
  8. 8.
    S. Eilenberg and J.B. Wright Automata in General Algebras. Information and Control, 11(4):452–470, 1967.CrossRefGoogle Scholar
  9. 9.
    G. Malcolm Data Structures and Program Tansformation. Science of Computer Programming, 14 (1990) 255–279CrossRefGoogle Scholar
  10. 10.
    C. E. Martin Preordered Categories and Predicate Transformers D.Phil thesis, Computing Laboratory, Oxford (1991).Google Scholar
  11. 11.
    O. de Moor Categories, Relations and Dynamic Programming D.Phil thesis. Technical Monograph PRG-98, Computing Laboratory, Oxford (1992).Google Scholar
  12. 12.
    O. de Moor Inductive Data Types IPL? (to be added) (1994)Google Scholar
  13. 13.
    C.C. Morgan Programming From Specifications (Second Edition) Prentice-Hall, Englewood Cliffs, NJ. (1994)Google Scholar
  14. 14.
    C.C. Morgan, K. Robinson and P.H.B. Gardiner On the Refinement Calculus PRG Technical Monograph PRG-70, Programming Research Group, Oxford (1988)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Clare Martin
    • 1
  1. 1.University of BuckinghamBuckinghamUK

Personalised recommendations