Are the authors setting forth yet another formal notation? We already have too many. But this well-written book is not about a notation: it is about formal specification and design, using the language COLD-K as a vehicle to represent concepts.
The first two parts have identical structures. They introduce a specification approach, and show how to set up a specification, how to structure large specifications, and how to implement a specification. The approach is algebraic in Part 1 and state-based in Part 2. The final part, “Advanced Techniques,” treats foundational topics, additional language constructs (including object creation), and large systems.
The authors describe algebraic and state-based specification clearly and succinctly. The emphasis is on the motivation for and use of formal specifications. Although syntactic sugar is shown, it is not overemphasized, and the readability of a specification is an important concern. The authors recommend having an informal understanding of sorts, predicates, and functions (for algebraic specifications) before trying to formalize them. The first point to check about a specification is its validity--“does the formal specification correspond with our intuition about the subject matter?” Design considerations that show, for example, how to avoid various anomalies are often explicitly addressed. The first sizable example in chapter 1 shows a path from a naive (defective) specification through improvement steps to the final specification (and discusses such concepts as “no junk” and “no confusion” axioms). This approach is used systematically in numerous examples throughout the book, leading to clear explanations--not ready-made solutions taken out of a hat.
After presenting sizable toy examples, the authors show structuring facilities essential for understanding (writing, reading, and reusing) specifications of realistic size. These facilities--modular specifications called “schemas” with possible explicit export and import lists--are used both for algebraic and for state-based specifications. This approach leads to the creation and reuse of a class specification library. The authors clearly state that no standard recipe for setting up large specifications exists, although useful guidelines and insights are given.
The last chapter of Part 1 shows how algebraic specifications can be systematically transformed into algorithmic implementations. These implementations use nondeterministic expressions. The largest example in this chapter shows how to implement an algebraic specification of sets in terms of a Pascal abstract data type list. The Pascal code is close to the specification of sets in terms of lists. Within this context, the authors stress the importance of the concept of “state,” which should not be restricted to the target language.
Part 2, on state-based specifications, starts by providing a path from algebras to states. The goal is to introduce a unified view rather than consider algebraic and state-based specifications as completely separate (as often happens). This unified view is obtained by generalizing some concepts from Part 1 and adding new concepts, such as procedures--special operations that perform state transitions. Dynamic logic (a generalization of Hoare logic) is used to specify procedures. Dynamic aspects of a system are specified in the usual declarative manner, by means of preconditions, postconditions, and invariants. The authors distinguish between an axiom (which holds in all states) and an invariant (which holds before and after execution of any of the given procedures, but may be temporarily violated in their intermediate states). Part 2 concludes with a chapter on implementing state-based specifications. An extended example is provided where COLD-K is used to express the algorithm, which is then translated to C.
Part 3 presents more advanced topics, both theoretical and practical. Chapter 9 deals with diverse theoretical issues, including a more formal description of meaning; a comparison between the initial algebra approach and the COLD-K approach of using loose semantics; a technical treatment of Horn clauses; and a discussion on finding the defining occurrence of a name. Chapter 10, “Additional Language Constructs,” describes an interesting scope extension; generic (parameterized) schemas with formal parameter descriptions; and classes with variable sorts used in object creation. Finally, chapter 11, on large systems, shows how further abstraction mechanisms including precisely defined graphical representations of reusable specification components may be used to enhance understanding. This chapter also provides a short overview of numerous practical applications of COLD-K.
Some minor shortcomings are as follows. In the traffic light example (section 6.2), a realistic, although abstract, software specification is presented, so the authors’ statement that the example “has very little to do with software specification” is incorrect. With a precise and complete specification, the notion of a “side effect” referred to by the authors in their description of a procedure (and a statement) seems to become quite different from its traditional counterpart. The book starts with a justification referring to the need for abstraction and precision. This approach is correct, but the role of others (like E. W. Dijkstra) in bringing these ideas to the attention of the readers is not explicitly mentioned. Perhaps the authors consider such general historical remarks unnecessary.
Mathematical maturity is clearly a prerequisite, but the concepts used by the authors are explained in the book; no particular knowledge is needed. A reference list of 58 items is included. The names of functions and predicates defined in the book are not included in the book’s index. Their inclusion would have been helpful, especially for reading large specifications. This book is a good introduction to formal specification concepts. It is very readable and elegant. It may be used in an almost notation-independent way, not just by those who are interested in the COLD-K notation.
