A working relational model: The derivation of the Dijkstra-Scholten predicate transformer semantics from Tarski's axioms for the Peirce-Schroder calculus of relations

Abstract

The definitions for Dijkstra's predicate transformer semantics can be justified by considering the meaning of a program as a binary relation on states (which holds between two states if there is a terminating computation connecting them) together with a set of states (those which initiate eternal computations). In fact, all of the definitions can be proved as theorems, using Tarski's ten equational postulates for the calculus of relations. These postulates define relation algebras, so we take the meaning of a program to be a pair of elements of a complete relation algebra, one corresponding to the binary relation determined by the terminating computations, the other corresponding to the set of states initiating eternal computations. The predicate transformers for a program are defined from these two elements. In this abstract setting we derive all the significant definitions and theorems of Dijkstra and Scholten's "Predicate Calculus and Program Semantics''.