home > book reviews > Edsger W. Dijkstra
Google > Edsger W. Dijkstra


Books

Short works

Books : reviews

Edsger W. Dijkstra.
A Discipline of Programming.
Prentice Hall. 1976

A Discipline of Programming is based on the author’s well-tested conviction that a carefully chosen separation of concerns is essential in every respect for the design of high-quality programs. Here he focuses on and solves, with fresh insight and originality, a separate problem of design in each chapter.

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.

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.