Academic Journals Database
Disseminating quality controlled scientific knowledge

Involutions on Relational Program Calculi

Author(s): I.M. Rewitzky | J.W. Sanders

Journal: Scientific Annals of Computer Science
ISSN 1843-8121

Volume: 18;
Start page: 129;
Date: 2008;
VIEW PDF   PDF DOWNLOAD PDF   Download PDF Original page

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.

Tango Rapperswil
Tango Rapperswil

RPA Switzerland

Robotic Process Automation Switzerland