R. D. Tennent
School of Computing
Queen's University
Kingston, Canada

Published February 2002 by Cambridge University Press (New York), and April 2002 by Cambridge University Press (Cambridge, U.K.), ISBN 0-521-00401-2 (paperback) and 0-521-80814-6 (hardback).

From the back cover:

This innovative volume provides a hands-on introduction to techniques for specifying the behavior of software components. Featured topics include techniques for using programmer-friendly assertional notations to specify, develop, and verify small but nontrivial algorithms and data representations, and for using state diagrams, grammars, and regular expressions to specify and develop recognizers for formal languages.

The presentation is based on numerous examples and case studies. It is appropriate for second-year and third-year computer science and computer engineering students familiar with basic concepts of discrete mathematics and logic. Using this book will help readers improve their programming skills and develop a sound foundation for subsequent courses in advanced algorithms and data structures, software design, formal methods, compilers, programming languages, and theory.

Excerpts from a review in Computing Reviews:

... a very readable text ...

... a genuine blend of mathematical rigor and informal but factually precise comments, which explain not only what the steps in the verification process are, but also, importantly, why any particular step is necessary.

... I would like to single out both the author's approach and his style of presentation as very positive features of the book. Reading this book is definitely inspiring, and not just for a student. As a lecturer of similar courses, I appreciate the book's pedagogical novelties.

P. Navrat, Computing Reviews, September 2002
Excerpt from another review in Computing Reviews:

The book contains a well-designed set of examples and assignments. It would be very useful for a course that expands beginner students' capabilities in programming, specifications, and algorithms.

David A. Gustafson, Computing Reviews, December 2002




Program 3
These are the headers and definitions assumed in program examples in the book. Students and instructors would want to include this file into their programs.

Appendix A
This is a compact reference manual (in PDF) for the small fragment of C/C++ used in the book. It may be used on-line if your browser has been assigned a PDF viewer as an application or plug-in for .pdf files.

PDF viewers for most platforms are available here: