*A Discipline of Programming*. 1976*Predicate Calculus and Program Semantics*. 1990, with Carel S. Scholten

- The Tide Not the Waves. 1997. (In
*Beyond Calculation*) - A formula is worth a thousand pictures. 2000. (In
*Millennial Perspectives in Computer Science*)

Rather than choosing one of the existing programming languages to work with, he has designed a mini-language that helps to stress the more fundamental aspects of the programming task. It facilitates nontrivial, satisfactory designs, enabling the user to go to the core of the problem quickly without getting caught up in the intricacies of handling a more complex language.

Stressing the formal aspects of correctness proving and program derivation,
as well as the formal aspects of problem solving, the book:

• Introduces “predicate transformers” as a means for defining the semantics of programming languages.

• Derives theorems about alternative and repetitive constructs that are functionally valuable in program composition.

• Emphasizes the necessity of *total* correctness.

• Spotlights the intertwined processes of problem solving
and program development in a series of efficiently worked-out examples.
For longer programs that solve more difficult problems, it records fully the true design history.

Written for those with a basic knowledge of computer programming, this book points the way toward future refinements in methods and accuracy through the time-honored approach of treating complicated problems in a simplified manner.

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.