Formal specification methods are gaining in importance as tools supporting the specifier are becoming available. This book describes Larch, a system of languages and tools for formal specification. Each Larch specification is written in two languages. The Larch Shared Language (LSL) is independent of any programming language and is used to describe an equational (algebraic) specification. An interface language links this level and a concrete implementation language and includes operational aspects; it allows the specifier to select special implementations of data structures, and its compiler automatically generates the module structure that is typical of the implementation language. This separation takes into consideration that communication mechanisms, such as module structure, parameter passing, and exception handling, differ from programming language to programming language. The book presents two implementation languages, LCL for C and LM3 for Modula-3.

After two short chapters summarizing the role of specifications and the notions of logic that are used in the remaining chapters, the third chapter gives a survey of Larch, illustrating it with a few small examples. The example specifying the operations on an indexed table is worked out in detail. The authors illustrate how to use assumptions about which concrete data structures are valid representations of abstract data structures. The next chapter provides a tutorial introduction to LSL. The basic unit of specification is a trait that specifies an abstract data type by introducing the operations, together with their signatures, and by giving a set of equations. Traits can be combined in a hierarchical way and can be parameterized. (Validation of a trait is simplified by assumptions on the behavior of the included traits.) Two special constructs allow strengthening the specification: the generated by clause defines a subset of operators sufficient to generate all elements of the data type, thus allowing the proof assistant to use an induction schema. A partitioned by clause enumerates those operators that lead to distinct values of the sort; this clause implicitly adds a deduction rule to the specification. Implies clauses specify additional properties; checking them during validation may uncover some deviation from the specifier’s intention.

Two chapters on interface languages follow. Chapter 5 considers the interface language for C, and chapter 6 considers the one for Modula-3. Each module consists of an interface and an implementation. The LCL interface specification is a formal description of the types, functions, variables, and constants provided for clients, together with comments providing informal documentation. Types, variables, and constants are defined by the usual C declarations. The behavior of functions, however, is described by preconditions that the implementor may assume to be true on calling the function and by postconditions that she or he must guarantee. From the LCL specification, a typical header file can be automatically derived, whereas the implementation part must still be provided by the implementor. The authors illustrate the features of LCL by presenting and discussing a complete specification of a small employee database. (The complete implementation is given in the appendix.) While LCL is presented in enough detail, the chapter concerned with LM3 is very short.

Since the Larch style does not emphasize executability, the specifier has to state precise claims that can be verified statically. Chapter 7 discusses the principal tool for this, the Larch proof assistant LP. First, the authors address the semantic claims about LSL traits, which fall into three categories: consistency, theory containment (intended consequences), and relative completeness. They give examples of how to represent them in the specification and summarize the proof techniques used. A special section shows how the LSL checker extracts proof obligations from the hierarchy of traits. The proof mechanism uses automatic normalization, application of deduction rules, critical-pair equations, and the Knuth-Bendix completion procedure. Other sections consider checking theory containment and consistency in detail. Finally, the authors present the results of checking a preliminary specification and show the usefulness of such a system during the development of a specification.

Chapter 8 is a short conclusion summarizing the essence of Larch. The appendix includes the complete definition of LCL and the implementation of the LCL interfaces in C.

The book is a clearly written survey and gives a good impression of the Larch system. It includes a comprehensive list of references, but not exercises. I recommend it to software developers who are familiar with the foundations of algebraic specification and with C.