The formal verification of sequential programs by means of syntax-directed proof systems is now well understood in principle. It is possible to take the proof rules as defining the semantics of the programming languages, and this is how Dijkstra defines the semantics of his language of guarded commands. A more state-oriented model (denotational or operational) is more appropriate from the point of view of language design and implementation, however, and this raises the question of the soundness of the proof system with respect to the chosen semantics.

In this book, a uniform approach is applied in turn to several classes of programming language, in order of increasing complexity. For each class, Hoare-style proof systems for both partial and total correctness are presented, and their soundness is established with respect to a structural operational semantics in the style of Hennessy and Plotkin. Examples illustrate the application of the various proof systems to simple problems.

The book is aimed at final-year undergraduates and graduate students and is intended to be suitable for use in courses on program verification or program semantics. It is organized in four parts.

The first part contains introductory examples and definitions and presents the syntax used for assertions throughout the remaining chapters. Part 2 is concerned with sequential programs, restricted initially to the deterministic case but later expanded to incorporate nondeterminism. The final sections are devoted to fairness, using a transformational method due to the authors.

Part 3, which forms the core of the book, is devoted to parallelism. It begins by considering the simple case of parallel programs whose components cannot interfere with each other’s variables, and then deals with the more difficult case of shared variables. The approach uses the notions of atomic action and interference freedom and is closely based on the work of Owicki and Gries (which was, however, confined to rules for partial correctness and did not extend to considerations of semantics or soundness).

In Part 4, a modified subset of Hoare’s CSP is used to represent a class of distributed programs. The techniques and examples are confined to ad hoc verification of programs that are already complete: the authors acknowledge this limitation, saying that they are aware of few examples of concurrent programs constructed in a systematic way from their specifications. A transformation of distributed programs to nondeterministic programs plays a key part, by enabling total correctness arguments to be decomposed into proofs of partial correctness, absence of failures and divergence, and freedom from deadlock.

The presentation is clear, if a little terse in places; the references are numerous and up to date, and the examples are well chosen. The book is largely successful in combining ideas and results from a variety of sources into a single unified framework, and should prove a useful reference. I am less sure of its suitability as a textbook. Selected sections could indeed, as the authors suggest, form a coherent course on program semantics or the theory of program verification using Hoare logics, and the numerous exercises would be more than adequate for this purpose. The sheer number of systems dealt with, however, means that it would be unreasonable to expect students to become skilled users of any of them. While Parts 1 and 2 would be accessible to undergraduates with a strong mathematical background, the more difficult later sections would be more appropriate to graduate students.