A specification of an abstract data type is defined by both a syntax and a semantics, and is basically a description of a class of objects in terms of their properties. The syntax defines the form of the specification, and the semantics defines its meaning, by associating an abstract data type with each specification. This advanced textbook is divided into five parts, each containing several chapters. Each chapter covers a single topic and concludes with a set of exercises.
The five chapters that make up the first two parts contain introductory material and necessary mathematical concepts. These five chapters occupy almost half the text and include topics in many-sorted algebras, structuring algebras, signatures, and logic. These subjects are often couched in terms of category theory and are generally difficult for nonmathematicians to follow. Though this text attempts to avoid such difficulty, it will not be easy reading for the average student, because it still involves a lot of math. Readers should have had one or two courses in abstract mathematics before approaching this text. The authors do an excellent job of presenting the essential mathematical tools, but that does not mean that the book is for everyone. It should be the basis for a course only at the advanced undergraduate or graduate level.
The third part of the book covers specification in the small. That is, it concentrates on specifications that are built from scratch. There are three chapters in this part, each leading to a different kind of atomic specification. Chapter 6 covers loose specifications, which are not bound to a specific logic and which define polymorphic data types. Chapter 7 discusses initial specifications, which require the use of a specific logic and define monomorphic data types. Most initial specifications use equational logic. Both of these types of specification have model-theoretic semantics. Constructive specifications, covered in chapter 8, are built using induction. The material on this method is an overview, since no standard definition of constructive specifications has been agreed on.
The fourth part deals with specification in the large. It consists of two chapters on theory and a final chapter that contains a complete case study. It is concerned with building large specifications from small specifications. The methods in Part 3 produce the small specifications that are used as the basic building blocks here. Chapter 9 deals with specification language constructs in much the way that one would discuss programming language constructs (rather than specific syntactic structures). However, the syntax for a small specification language is developed as part of the discussion. Chapter 10 discusses extensions necessary for modularization and parameterization. These extensions are needed for the creation of useful, reusable specifications that deal with real problems. Chapter 11 is a case study of building specifications for a lexical analyzer in the style of LEX.
The final part consists of a single chapter, divided into sections that provide short introductions to a number of related topics.
Because my background is in abstract mathematics, I found this text easy to follow. The authors have done an excellent job of producing a self-contained, readable volume. The exercises are generally well thought out. However, my current interest is in software engineering, and I am not sure what my students would take from this text that is useful in a day-to-day job situation. Most of my students are more engineering-oriented; they would probably be willing to use a tool based on the material in this text, but would not be interested in the theory that went into producing the tool. I would have liked to see more examples. I like the book and think serious students of software engineering should spend some time with it, because it will help them understand specifications.
