zbMATH — the first resource for mathematics

Fundamentals of algebraic specification 1. Equations and initial semantics. (English) Zbl 0557.68013
After a decade of development, there are now many results in the theory of algebraic specification of abstract data types, and it is time now to organize and present the material in comprehensive textbooks. The present book is the first of two volumes supposed to cover a great deal of the theory. The viewpoint taken is, one may say, the classical ADJ-viewpoint, heavily emphasizing initial algebra semantics of equational specifications. Accordingly, the present first volume treats equations and initial semantics as the most basic parts of the theory. Volume 2 is announced to cover formal requirements and modules. Also, there are plans to publish a supplementary third volume by another author in the same series where the connections between specifications, interpretations, implementations, and programs in programming languages will be elaborated.
The contents of the present book is organized in eight chapters plus a two chapters appendix. The level of the first wo chapters is somewhat more elementary than the rest. Starting with examples showing the use of equations for specifying classes of algebras, an elementary introduction to algebras, terms, data types, abstract data types, and correctness is given. Chapter 3 studies initial semantics of equational specifications from an algebraic and sometimes also categorical point of view. Chapter 4, in contrast, assumes loose semantics and discusses specifiability by presenting Birkhoff’s characterization of equational classes. Chapter 5 gives an extensive treatment of equational calculus and (symmetrical) term rewriting (the theory of directed term rewriting, including normal forms, confluency, etc. is not treated in the book). Chapter 6 on correctness and extensions of specifications addresses more pragmatic questions. Chapter 7 and 8 presents the theory of parameterized specifications, their semantics in terms of functors and parameter passing. The appendix, consisting of chapters 9 and 10, presents concepts, syntax, and formal semantics of the specification language ACT ONE.
The merit of this book is that it is the first presenting the theory in some depth (there was an earlier introduction by H. A. Klaeren [Algebraische Spezifikation - eine Einf├╝hrung. Springer-Verlag (Berlin 1983; Zbl 0506.68009)] in German, going not very far in this respect and putting a different emphasis). Thus, much material is now easier accessible as it as before. Accordingly, the book is especially useful for people who want to enter the field, but also as a reference for people working in the field (there are some etails nicely cleaned up that were treated somewhat sloppily before in the literature).
The text of the book is carefully prepared and provides some comfort for readers. The printing, however, using small letters and very limited character set of a conventional typewriter, is uncomfortable to read. The non-numbering of sections makes it sometimes difficult to locate specific spots in the book.
Reviewer: H.-D.Ehrich

68-02 Research exposition (monographs, survey articles) pertaining to computer science
68N01 General topics in the theory of software
68Q60 Specification and verification (program logics, model checking, etc.)
68P05 Data structures
08B05 Equational logic, Mal’tsev conditions
08C05 Categories of algebras
18C05 Equational categories