Browse Books

Reviewer: Jacques Jean Arsac

A program consists of statements designating the actions to be performed and the variables on which they operate. Each statement changes the state of variables, which may be defined by an assertion, that is, a relation between variables that must be true at a particular point in the program. Each statement is an assertion transformer, and the transformation it performs is its semantics. To verify a program, one must prove that the final state resulting from these actions upon the known initial state is the desired state. This is the background on program verification presented in this book. The authors take a formal approach: instead of presenting assertions using a combination of plain English and mathematical notation, they use only mathematical formulas with quantifiers. The semantics of statements are given as substitution rules in mathematical formulas. A sequential program is partially correct if it gives the desired result each time it terminates; it is totally correct if it terminates with the desired result for all data in the appropriate domain. Proof techniques are given. It can be difficult to find efficient assertions for a program once it has been written. The best approach is to start with assertions and derive the program from them. A nontrivial classical program is presented to illustrate this method of programming. Disjoint parallel programs consist of components that have only read access to their common variables. The authors show that they can be replaced by equivalent sequential programs. Auxiliary variables can be used to simplify verification. The verification of disjoint parallel programs is illustrated by a case study. The verification of parallel programs with shared variables is more difficult: a shared variable may be changed by one component of the program while it is being processed by another. The authors introduce auxiliary variables so that each assignment implies only one shared variable. Rules of verification are given, and examples are discussed. In many applications, parallel components must be synchronized, with one having to await the result of another. Deadlock occurs when a component does not terminate, and the other components of the program are awaiting its result. Weak forms of correctness are introduced for components of parallel programs. A producer-consumer problem is discussed as an example. The problem of the use of a common resource by several programs has been solved using semaphores. Parallelism introduces nondeterminism into programming. Guarded commands provide a model for nondeterministic programs. Distributed programs can be transformed into nondeterministic programs. The authors discuss the concept of fairness for parallel programs: each component progresses with unknown but positive speed and will eventually execute its next enabled atomic statement. Several case studies are discussed. This is a good introduction to program verification, an essential issue in programming. The authors present a unified approach, from sequential programs to distributed programs, using the same formal system for all kinds of programs. Partial and total correctness are discussed, though nothing is said about program complexity. Every book on this subject has a pedagogical difficulty: if the examples are simple enough to be discussed easily, the reader will get the idea that only toy programs can be derived and verified, and that the method cannot be used for real-life programs. If more complex programs are discussed, the book becomes too long and possibly tedious. Most of the examples used in this book are extremely simple, used only to make the formalism clear. The authors' case study of a sequential program is not very convincing, perhaps understandable in a book whose main object is parallelism. The case studies of parallel programs are more convincing, because they are closer to real-life models. They can be used as models for everyday programming. The authors include appropriate references, including books published in the 1970s, the object of which was to transform programming from an empirical, trial-and-error activity in to a science. It will serve as an excellent textbook for students of programming.