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)


  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}