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.