Cohen was strongly influenced by such people as Feijen, Gries, and Dijkstra. As a result, the flavor of this introduction to computer programming is theoretical. It is not tied to any particular language. The author suggests that it be used to introduce programming to students in their first year. Though he does suggest that it would be possible to learn Pascal in parallel or to translate the notation into another language, he clearly would prefer that the student cover at least half the book before using an actual language.

If your students have a good background in mathematics prior to being taught programming and are motivated by mathematical examples, you will find this to be one of the better introductory programming books available. For most students, previous work in a language such as Pascal is desirable. Such experience should provide concrete examples of the concepts in this book, and aspects of the language that ignore or contravene the structure should not be taught. It is likely that Cohen’s students who used the book originally were not novices, given that he assumes familiarity with such data structures as customer databases (chapter 4). Similarly, it would be nice to have a subsequent book that took the application of material out of the toy program range into applications in the real world.

Cohen commences with a motivational chapter of introductory material (chapter 0), followed by a discussion on the careful proving of a theorem (chapter 1). The discussion assumes that the reader is sufficiently mathematically sophisticated to appreciate, and be able to use, axioms in proofs. Given that, the explanation is clear and detailed.

Chapter 2 introduces the manipulation of predicates. No attempt is made to relate the results to any concrete realization. Indeed, Cohen points out that manipulating predicates is fun, and proficiency in this area will be useful later. He introduces and manipulates the various Boolean operators. In a similar vein, quantification of expressions is introduced in chapter 3. On only a few occasions is the discussion related to actual operators and quantifiers.

Chapter 4 provides meaning to the operators and quantifiers so that programs can be specified. The notation used is a Hoare triple. The author gives many examples of specifications. Chapter 5 covers the shape of programs that include assignments, alternation, and repetition. Chapter 6 pauses to examine proofs and calculations.

Programming is commenced in chapter 7, where assignment and *if *statements are introduced into loopless programs. The chapter covers calculation of expressions in assignments and the solution for guards and determinism.

Loops are introduced in chapters 8, 9, and 10. In chapter 8 the invariance theorem is invoked to provide the loop invariant. The precondition and postcondition are set; the invariant has to be chosen, followed by the bounds and loop body. Chapter 9 applies these principles to integer division, linear search, and 3-tuple sort. Chapter 10 introduces fresh variables that link the invariants of a loop. Polynomial evaluation and linear search are just two of eight examples.

Tail recursion is defined in chapter 11. Some of the functions given are not tail-recursive. In that case, a transformation of the problem into a more general tail-recursive function is necessary. Chapter 12 recaps the design process.

Exercises are liberally scattered through the text, but no sample solutions are given. The index appears to be reasonable, though I was unable to find the words “fresh variables,” from the title of chapter 10, under any likely heading. The bibliography is up to date. A majority of the references are to books and papers by Dijkstra, Feijen, Gries, and Hoare.