Browse Books

Reviewer: Ali Mili

The first paragraph of the preface starts the book off on a very upbeat note: This book is about specifications of computer programs, but it is not a book about a specification method, a specification language or a specification technique currently on the market. It is not even about any of these things as they may become available in the future. The main purpose of this book is to explain the nature of specifications. Thus it is a book about such aspects of specifications as are inherently there, even if a particular presentation chooses to ignore them. The field of program specification has reached such a level of development and maturity that one can write a whole book doing nothing more than explaining the nature of specifications. To its credit, this book does so with a great deal of precision and some humor. However, the claim in the preface needs a number of adjustments. First, the book is oriented toward a particular aspect of specifications and hence has a less general scope than the authors acknowledge. Second, perhaps inevitably, it is also biased toward a particular specification language. Third, it oversteps the boundaries of program specifications and moves into such areas as program design and implementation. I will discuss these adjustments in turn below. It is only halfway through the book (which may be half a book late) that the authors acknowledge the existence of two possible emphases in a specification: It is a matter of choice as to what is the main emphasis of specification: it may be mainly property-oriented (e.g., when it specifies a data type) or relation-oriented (e.g., when it specifies desired reactions to envisaged events). While the differences between the two kinds may seem large and could be exaggerated by the choice of different formalisms for recording G, the principal methodological aspect is the same: one way or another, G is the base for reasoning about all objects that conform to G, where G is a specification (set of formulas) being discussed. Of course, one can hardly argue with the unifying and appealing view presented here; nevertheless, to the extent that the business of specification is not mere representation but mostly reasoning, a specification formalism is still better adapted to specifications for which it provides better mechanisms for tackling complexity. It is fair to say, I think, that this book is geared toward property-oriented specifications; while this is not a shortcoming, the presence of a clear statement about the matter is desirable. While, to the book's credit, most of the discussions on program specifications are language-independent, there are instances when, perhaps inevitably, the subject matter is a specification language. In particular, Burstall and Goguen's language Clear gets some attention and is used for illustrative examples. The third modification that needs to be made to the claim of the preface is that the book discusses not only program specification but also program design and implementation. Of course, the relationship between specification and design is too close for one to be able to talk about one without the other; on the other hand, their dividing line is too unclear for one to determine where the discussion of specification ends. In addition to the brief software engineering preliminaries in chapter 1, the book contains three main chapters. Chapter 2 discusses mathematical preliminaries to program specifications; it includes background from the theory of computation and mathematical logic. Despite its difficult subject, this chapter is easy to read because of the liveliness of its presentation. Chapter 3 discusses the relationships between specifications and programs; the notion of program correctness with respect to a specification is of particular interest. The tone of this chapter is, at times, rather convoluted; this is especially annoying where formal definitions are expected. However, this may result from the book's concern for generality, including specification language independence and programming language independence. Chapter 4 deals with program design. It is very well organized. It discusses several aspects of stepwise refinement, illustrates them with judicious examples, and analyzes their impact in terms of property preservation and addition of detail. This chapter also highlights some key design principles in a very cogent manner; particularly noteworthy is how the principle of postponing design decisions is illustrated by means of examples. Finally, a lengthy appendix gives a complete, if dry, overview of the mathematics of program specifications. The style of the book is pleasing; it is fairly rigorous, easy to read, and free of idioms. The book has an index and a selected bibliography. The bibliography contains references that share the same concerns and orientation as the book; I would suggest inserting the proceedings of an ACM- and IEEE-sponsored workshop series on software specification and design (Kyoto, 1982; Orlando, 1984; London, 1985; Monterey, 1987; and, upcoming, San Francisco, 1989). Another comment on the bibliography is that the references are not always available. The preface admits that This book is not a textbook in the widely accepted sense. There are no exercises or other easily noticeables feature of a good textbook. Neither is this book a monograph, as it does not develop a monolithic view of a subject. It is much closer to the idea of a reading book, or collection of essays, on the subject of specification. The promotional text on the back cover adds, “The book will be suitable as a supplement for Computer Science students taking advanced courses in Software Specification, Software Development or Software Engineering, and will also interest professional programmers who need a guide to specification and its relationship with program development.” I agree with both assessments and intend to use the book as a supplementary text for a graduate-level course on software development. Thanks to its rigor, precision, and generality, this book will be of interest to researchers, teachers, and students. On the other hand, thanks to the maturity of its ideas, it will also be of interest to practicing software engineers.