Browse Books

Reviewer: Lars Langemyr

The authors describe recent progress in the area of formal methods for software development. They focus on algebraic techniques for specification, an area in which they have contributed substantially to recent developments. They do not discuss formal methods for software development in general. They point out that the methods described in the book are not yet ready for practical application to program development. This book is the second in a series on algebraic specification techniques. The first volume [1] covers basic equational reasoning and how it can be applied for formal specification. The authors have a certain semantic model (initial semantics) in mind, and they convincingly show its advantages. This book focuses on the concept of a module, which allows a further level of abstraction by hiding internals of a specification (compare the module concept of Modula-2 or packages in Ada). A better structuring can often be achieved by using the module concept. The book is the first complete guide to this new research area. Chapter 1 informally presents the concept of an algebraic module and gives some historical background. A module consists of four specification parts—import interface, export interface, parameter, and body part. Chapter 2 gives a formal definition of module specification with syntax, semantics, and correctness. Morphisms between the four parts give two alternative semantic notions—functorial and restriction semantics. The third chapter introduces operations on module specifications. The operations are composition, union, and actualization. The authors show that these operations preserve correctness and semantics. Chapter 4 generalizes the concept of operation on a module, showing that the previous operations on modules are only instances of the new concept. In Chapter 5 the authors discuss how an interface consisting of export, import, and parameter parts can be extended to a complete module specification, including a body. This extension is called realization. They also show that refinement of a module is compatible with the module operations from chapter 3. Chapter 6 extends refinement to the general module operations of chapter 4. The seventh chapter introduces the concept of constraint in order to increase the power of a module specification by extending the power beyond equational logic. In Chapter 8 the authors extend the concepts from chapters 2 and 3 to the case where constraints are allowed in the parameter, import, and export parts of a specification. In chapter 9 they define two specification languages that realize the ideas of previous chapters. Chapter 10 provides a summary of basic notation. The book is clearly written and gives an intuitive explanation for most concepts and ideas. Sometimes, however, the reader gets a feeling that the notation will become less complicated when further research has been done. The book is suitable for a graduate course in algebraic specification or for someone intending to do research in the field. A disadvantage for course use is that the book includes no exercises; it contains illuminating examples, however. The first book in the series [1] is a necessary prerequisite. Previous experience with universal algebra makes reading easier. The authors provide a summary of basic notation, a bibliography that covers recent work in the area, and a short subject index.