The content of this brief book is accurately described by its title and subtitle. It mostly confines its attention to “operational” forms of programming-language semantics, emphasizing structural induction as a technique for constructing soundness proofs. The preface states that the academic level is lower-division undergraduates and that “students who have undertaken an introductory programming course and who are familiar with elementary mathematical notation should have little difficulty in following it.” This low level of difficulty sets the book apart from others in its field.

Hennessy introduces many small programming languages to provide a basis for illustrating various concepts of semantic definition. The language Exp consists of simple arithmetic expressions. Exp2 is Exp with variables, Exp3 is Exp2 with scoping, and Exp4 adds Booleans and conditionals. Fp1 is Exp4 with functions. CalcL is a calculator with a rudimentary state. The StreamL language consists of infinite sequences, WhileL implements imperative features, GuardL is a language for nondeterministic guarded commands, and ParL provides OCCAM-like parallelism.

Abstract syntax and structural induction, which play a central role throughout the book, are introduced in chapter 1. Using Exp as a sample subject language, chapter 2 lays out a spectrum of methods of semantic formalization. In order of increasing abstraction, these semantic models are concrete operational semantics, computation semantics, evaluation semantics, and denotational semantics. In the author’s presentation, however, evaluation semantics precedes computation semantics. The denotational approach is described cursorily because the book’s focus is on the three operational models. “Concrete operational semantics” is Hennessy’s term for the old-style methods that make use of abstract machines. In a “computation semantics,” the individual small steps involved in a program’s execution are described mathematically. In an “evaluation semantics,” the specifications are concerned with the overall process of producing final results.

Chapter 3 develops an evaluation semantics for the functional language Fp1, using Exp2, Exp3, and Exp4 as stepping-stones. The emphasis on evaluation semantics continues in chapter 4, where the subject languages are CalcL, StreamL, and WhileL. Chapter 5 shifts the reader’s attention to the less abstract models, developing computation-semantics specifications for Fp1 and WhileL and a concrete operational semantics for Fp1 in which the operation of the abstract machine is defined by a computation semantics. In chapter 6, the author develops computation-semantics formulations for GuardL and ParL.

On the whole, the book is clearly written and achieves its modest objectives. With the help of a knowledgeable instructor, students should be able to obtain a basic understanding of the formal semantics of programming languages. An ample number and variety of exercises appear at the ends of chapters. The references to other literature are adequate.

On the negative side, the book does have its share of typographical errors, including symbol substitutions and missing or added primes. In this area, unfortunately, such errors can greatly degrade understandability, especially for people trying to read the book on their own. The numerous “figures” consist entirely of text and, because they are not set in a different typeface, tend to derail the reader from the main discussion. The index is only one and one-half pages long. The softcover binding prevents the book from lying open on a flat surface.

The author makes a few comments that could be considered careless or controversial. For example, in chapter 1 he uses the term “parse trees” to refer both to derivation trees and to abstract-syntax trees, and on page 40 he speaks of a program being “compiled or interpreted into machine language.” On page 19 he seems to suggest that truth, in a mathematical system, is the same thing as provability. Some aficionados of the denotational approach may take exception to the assertion in the book’s penultimate sentence that “much of the need for denotational theories has been side-stepped,” but opinions such as this are contributions to the general debate. This book is a good introduction to recent developments in operational semantics.