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.

- Preface
- 1 The Paradigm Tirangle
- 1.1 Declaring the Paradigm
- 1.2 Classical Propositional
- 1.3 Modal Logic
- 1.4 Some Basic Ideas
- 1.5 Historical and Bibliographical Notes
- Examples and Exercises

- 2 Power Structures and Duality
- 2.1 Power Sets and Stone Duality
- 2.2 Power Algebras and Jónsson/Tarski Duality
- 2.3 Priestly Duality
- 2.4 Power Structures
- 2.5 Historical and Bibliographical Notes
- Examples and Excercises

- 3 Program Semantics
- 3.1 The Relational Model
- 3.2 Predicate Transformers
- 3.3 A Jónsson/Tarski Duality for Programs
- 3.4 Hoare Logic and Predicate Relations
- 3.5 Domains and Powerdomains
- 3.6 Information Systems
- 3.7 Historical and Bibliographical Notes
- Examples and Excercises

- 4 Verisimilitude
- 4.1 Verisimilitude via Power Relations
- 4.2 Verisimilitude via Powerdomains
- 4.3 Verisimilitude via Vietoris
- 4.4 Information and the Paradigm Triangle
- 4.5 Historical and Bibliographical Notes
- Examples and Excercises

- 5 The Relational Model as a Priestly Space
- 5.1 A Priestly Space of States
- 5.2 Properties of States
- 5.3 Programs as Input-Output Relations
- 5.4 Historical and Bibliographical Notes
- Examples and Excercises

- 6 Translations
- 6.1 From the Relational Model to Predicate Transformers, and Back
- 6.2 From Predicate Transformers to Information Systems, and Back
- 6.3 From Relational Model to Informational Systems, and Back
- 6.4 To the Smyth Powerdomain, and Back
- 6.5 Conclusion
- Examples and Excercises

- A Background in the Calculus of Binary Relations
- B Background in Lattice Theory
- C Background in Topology
- Bibliography
- Notation
- Subject Index
- Name Index

9/1/2001