In the “calculational style” of programming that is currently being promoted by Feijen, Dijkstra, Gries, and others, algorithms are derived from formal specifications, leading to programs that are correct by construction. Verification is a byproduct of this process. Kaldewaij presents program derivation as a creative process in which design decisions are based on considerations such as “efficiency, simplicity and symmetry.”

The author has used this deceptively compact book in a third-year course and in a one-year introductory course at Eindhoven University; the only prerequisite was an introductory course in Pascal. Her approach to using this book in the introductory course appears to be essential: a leisurely pace for lectures is combined with exercises that must be worked out “with great precision” in small groups. An instructor’s manual contains solutions to the exercises.

Technically, this book appears to be both conventional in its notation and topic selection and pleasingly motivational in its emphasis on applying theory to solving problems. Five introductory chapters on notation and computation are followed by seven chapters of applications and problem solving. Naturally, since I did not spend the recommended academic year to get used to the notation and accompanying rigor, I spent time checking that my understanding of the notation agreed with the author’s and working through examples. An appendix that defined the notations would help. Overall, I liked the book, especially because of the applications and problems.

My critical concern is not how well I like a book, but how well students will learn from it. In reading the sample derivations of programs, I encountered an alarming statement: “Needless to say that this program cannot be easily understood without its derivation” (p. 91). I consider this to be a serious flaw in the methodology. Solutions are often so creatively derived or so formally stated that the resulting programs require a thorough understanding of both their derivation and the formalisms used in their derivation before they can be comprehended or modified. Thus we arrive at a science of computing that requires very bright scientists with exceptional mathematical skill. Exams may also emphasize memorizing solutions in a manner reminiscent of my experience as a graduate student in mathematics.

The formal methods in this book may enhance reliability, efficiency, brevity, and scalability, but learnability and clarity suffer. If you are in the market for a book in this area, consider this one. The material is far more attractive as a third-year course than as a one-year entry-level course.