Books : reviews

Edsger W. Dijkstra, Carel S. Scholten.
Predicate Calculus and Program Semantics.
Springer. 1990

This book gives a self-contained foundation of predicate transformer semantics; it does so by making extensive use of the predicate calculus. The semantics of the repetitive construct is defined in terms of weakest and strongest solutions; in terms of the weakest precondition and the weakest liberal precondition, the notion of determinacy is defined; it is shown how to cope with unbounded nondeterminacy without using transfinite induction.

The book distinguishes itself from all other works on program semantics in that the approach is nonoperational: the definition is not in terms of a computational model. It distinguishes itself from many mathematical texts in that its proofs – which are short and elegant – follow a strict calculational format.

It is a monograph for computing scientists with a mathematical inclination, and methodologicaily interested mathematicians. It is not designed as a textbook, although successful courses have been given based on this material.