Published in Volume XVIII, 2008, pages 129-171

Authors: I.M. Rewitzky and J.W. Sanders


The standard Galois connection between the relational and predicate-transformer models of sequential programming (defined in terms of weakest precondition) confers a certain similarity between them. This paper investigates the extent to which the important involution on transformers (which, for instance, interchanges demonic and angelic nondeterminism, and reduces the two kinds of simulation in the relational model to one kind in the transformer model) carries over to relations. It is shown that no exact analogue exists; that the two complement-based involutions are too weak to be of much use; but that the translation to relations of transformer involution under the Galois connection is just strong enough to support Boolean-algebra-style reasoning, a claim that is substantiated by proving properties of deterministic computations. Throughout, the setting is that of the guarded-command language augmented by the usual specification commands; and where possible algebraic reasoning is used in place of the more conventional semantic reasoning.

Full Text (PDF)


[1] R.-J. R. Back. Combining angels, demons and miracles in program specifications. Theoretical Computer Science, 100(2):365-383, 1992.

[2] R.-J. R. Back and J. von Wright. Duality in specification languages: a lattice-theoretical approach. Acta Informatica, 27(7):583-625, 1990.

[3] R.-J. R. Back and J. von Wright. Refinement Calculus: a Systematic Introduction. Springer Verlag, 1998.

[4] P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, 238-252, January 1977.

[5] E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.

[6] E.W. Dijkstra and C. S. Scholten. Predicate Calculus and Program Semantics. Springer Verlag, 1990.

[7] W.-P. de Roever and K. Engelhardt, Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1998.

[8] P. H. B. Gardiner and Carroll Morgan. A single complete rule for data refinement. Formal Aspects of Computing, 5(4):367-382, 1993.

[9] G. Gierz, K. H. Hofman, K. Keimel, J. D. Lawson, M. Mislove and D. S. Scott, A Compendium of Continuous Lattices. Springer Verlag, 1980.

[10] C. A. R. Hoare et al. The laws of programming. Communications of the ACM, 30(8):672-686, 1987.

[11] C. A. R. Hoare and J. He, Unifying Theories of Programming. PrenticeHall series in Computer Science, 1998.

[12] J. Lambek and P. J. Scott, Introduction to Higher-Order Categorical Logic. Cambridge University Press, 1986.

[13] R. D. Maddux. A working relational model: The derivation of the Dijkstra-Scholten predicate transformer semantics from Tarski’s axioms for the Peirce-Schr¨oder calculus of relations. South African Computer Journal, 9:92-130, 1993.

[14] C. Morgan. Programming from Specifications, second edition. PrenticeHall International, 1994.

[15] J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287-306, 1987.

[16] G. Nelson. A generalisation of Dijkstra’s calculus. ACM Transactions on Programming Language and Systems, 11(4):517-561, 1989.

[17] O. Ore, Galois connexions. Transactions of the American Mathematical Society, 55:494-513, 1944.

[18] K. I. Rosenthal. Quantales and their Applications. Pitman Research Notes in Mathematics, 234, Longman, 1990.

[19] J.W. Sanders. Computations as fibre bundles. In Proceedings of Relational Methods in Computer Science 2006, edited by R. A. Schmidt, LNCS 4136:30-62, Springer-Verlag, 2006.


  title={Involutions on Relational Program Calculi},
  author={I.M. Rewitzky and J.W. Sanders},
  journal={Scientific Annals of Computer Science},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  publisher={``A.I. Cuza'' University Press}