The intended audience for this book is software developers working in industry or business. Accordingly, it takes a pragmatic approach to the use of proof rules in developing and proving programs. Many of the theoretical and practical complexities are not treated here, since the book is only an “initial introduction” to the material. The book gives proof rules for simple language constructs, shows how to use them in verifying the correctness of programs and in designing correct programs, and provides some guidance in the formulation of pre- and postconditions. The presentation is clear, and Baber provides many examples. Several standard programming paradigms are used as extended examples (such as linear search and searching for a substring).

As with many treatments of this approach, the discussions and proofs are so much longer than the program fragments being treated that a reader might well wonder whether the effort is worthwhile. Presumably this point must be addressed when the text is used in industrial courses. The book can be recommended as a readable introduction to proof rules for working programmers and undergraduate students.