A Paradigm for Program Semantics

This book provides a synthesis of four versions of program semantics. In relational semantics a program is thought of as a binary input-output relation over some state space; in predicate transformer semantics a program is a mapping from predicates to predicates; in information systems (and Hoare logic) a program is considered as a relation between predicates, and in domain theory a program is a multifunction mapping states to sets of states. Brink and Rewitzky show, through an exhaustive case study analysis, that it is possible to do back-and-forth translation from any of these versions of program semantics into any of the others. They do so by invoking techniques from non-classical logics, lattice theory, topology and the calculus of binary relations. At the heart of their method is the notion of a power construction, and an invocation of duality theory. A power construction lifts a given structure from its base set to its power set (the set of all its subsets); duality theory essentially then tries to recapture the original structure from the lifted structure. Specifically, the duality theory at work in this book is "Priestley duality", which identifies certain topological spaces ("Priestley spaces") as the duals of distributive lattices. In the authors' version, relational Priestley spaces are the duals of distributive lattices with operators.

The importance of the book lies in its demonstration that, although there are many variations of each of the four versions of program semantics, in principle they may be thought of as intertranslatable.

Chris Brink is the vice-chancellor of the University of Stellenbosch in South Africa. Ingrid Rewitzky is a lecturer in the department of mathematics and applied mathmatics at the University of Cape Town in South Africa.

Contents

9/1/2001