Any formal definition of a language has to clearly specify its syntax (a grammatical specification that in some way fixes the structure of well-formed statements) and semantics (the manner in which meaning is assigned to well-formed statements). To these one may also add the specifications of types, which restrict the language syntax in some useful way, and pragmatics, which can further restrict the use of the language to suit real-world considerations (such as some notion of propriety or efficiency). Such specifications of formal languages are at the core of much work in areas such as logic, computational linguistics, and the formal verification of hardware and software.

Syntax itself can be abstract or concrete, and is specified in terms of formal grammars, which are well known to be of four major types: regular, context-free, context-sensitive, and unrestricted. Semantics are also of various kinds: operational, denotational, and axiomatic. The various kinds of semantics are somewhat equivalent in scope in certain cases, but are not always exactly so.

The present book can be described as a specialized text dealing with the semantics of formal languages in various contexts. It is not one that deals with other topics in computation theory. The authors are highly regarded researchers and scholars in mathematical logic and such, but have adopted a light touch suitable for beginning graduate students and other nonspecialists, while still adhering to the standards of rigor that the subject demands.

The book consists of 16 chapters in five parts. Part 1 (two chapters) gives a broad introduction to formal language theory and related topics, and to preliminary topics in discrete mathematics and mathematical logic. Part 2 consists of four chapters, which formally define and use IMP, a “simple imperative language” that is meant to model the basic aspects of imperative programming languages, sans sophisticated constructs for data types, class definitions, object orientation, and so on. In addition to the definition and basic properties of IMP, this part also explains the operational and denotational semantics of IMP (to illustrate what these kinds of semantics mean) and the related concepts of induction, recursion, and fixpoints.

Part 3 (four chapters) introduces HOFL, a “higher-order functional language” used to illustrate concepts in operational and denotational semantics; of particular note is chapter 10, which shows the equivalence between the denotational and operational semantics of HOFL. Part 4 (three chapters) deals with concurrent systems (a legacy of the late Dijkstra), introducing the calculus of communicating systems (CCS) and its semantics, and also discussing the μ-calculus and the π-calculus in later chapters.

Part 5, “Probabilistic Systems,” consists of three chapters. The first two deal with “Measure Theory and Markov Chains” and applying Markov chains in the analysis of nondeterministic systems. The last chapter is a brief introduction to PEPA, a “performance evaluation process algebra.”

Regrettably, the book lacks a keyword index. Worse still, it also lacks a bibliography. In fact, the authors don’t discuss related works at all; doctoral students and others who want an in-depth understanding of the topic, with references to multiple sources of information, will most keenly feel this lack. However, instructors will welcome the end-of-chapter problems and appendix of solution hints to selected problems.