Foundations of Algebraic Specification and Formal Software Development (Monographs in Theoretical Computer Science. An EATCS Series) [Hardcover]

This is a great book, very well and concisely written, containing everything I ever wanted to know about algebraic specifications!

It gives a very nice introduction to universal algebra, category theory and equational specifications; it presents all about structured and parameterised specifications and their proof techniques, shows how to work within arbitrary institutions and multiple logical systems, and discusses formal program development and behavioural specifications. All concepts are well illustrated by small instructive examples, and I like also the precise bibliographical remarks at the end of chapter.

The "Foundations of Algebraic Specifications and Formal Software Development" are a must for everybody interested in learning about algebraic methods in software development.

The book gives a detailed and comprehensive overview of both algebraic specification and formal program development. This is remarkable, because many related works from the area of formal methods treat either only the specification side (which remains a bit fruitless since no relation to real computer programs is given) or only the formal program development side (which remains quite pragmatic, since only the behaviour of programs is specified, e.g. using a Hoare style logic, but without a possibility to specify the concepts that are modeled by the program). Hence, the value of the present work cannot be overestimated.

After a general motivation in chapter 0, algebraic specification is developed in chapters 1 and 2. Indeed, the term "algebraic" is a bit misleading here, since the general topic is axiomatic specification. This becomes even clearer in chapter 4, where (using a nice preparatory chapter 3 about category theory) the theory is generalised to an arbitrary logical system, formalised as institution. Here, the authors introduce a multitude of logical formalisms, notably first-order logic and a simple functional programming language called FPL, these two being at the heart of many examples in later chapters, and indeed, first-order logic is used for the specification part, while the functional programming language is used for the program development part. Indeed, this book is the second one providing an introduction to the theory of institutions, the first one being R. Diaconescu's "Institution-independent model theory". While Diaconescu's book takes more the perspective of a logician (although it also has many connections to computer science), the present book is more cleary grounded in and motivated by computer science.

Chapter 5 introduces structured specifications in the context of an arbitrary institution, and presents a moderately-sized example illustrating the practical use. Chapter 6 extends this with (higher-order) parameterisation, and carefully illustrates the difference between specification of parameterised programs and parameterised specification of programs. Chapter 7 then uses this to build the machinery for formal program development, which is illustrated with some larger example involving hash functions on two levels. The example is nicely chosen, although the notation for higher-order constructors is sometimes difficult to read. The authors eventually introduce the "given" notation, which is much more readable.

Chapter 8 extends the previous work to behavioural specifications, first for standard algebraic specifications, then for the programming language/logic FPL, and then for an arbitrary institution. This requires considerable technical effort, but the reader gets presented a formalism that both subsumes the many diverse existing approaches in the literature and that captures the relevant problems of data abstraction and behavioural encapsulation. Again, this is illustrated with the above mentioned example.

Chapter 9 provides proof systems at the various levels introduced so far, and (after a certain bias to particular institutions in chapter 8) continues the institution independent approach of the preceding chapters. Soundness and completeness is discussed and proved at the various levels, as well as illustrative examples are given.

Chapter 10 opens the perspective of working with multiple logical systems using institution morphisms and comorphisms, which gives rise to new heterogeneous specification constructs, that can e.g. be used for a more systematic relation of specification and programming languages.

The ten chapters provide quite a lot of material, leading to a quite thick book which most people probably won't read sequentially, but more selectively, or use it as a reference. The authors give some hints for selective reading and also for using the material in university classes.

The book benefits from lots of carefully chosen examples (specification and programs) at various places that click together at later stages. This makes the book really a computer science book, although it is quite mathematical. Still, it should be made clear that the book takes the perspective of *theoretical* computer science, and the examples, although some go beyond the size of small toy examples, are still far away from industrial case studies (and no link to such case studies is given in the book). Now such an application perspective heavily depends on the availability of good tool support. Many of the numerous example specifications provided in the book have been formulated in the Common Algebraic Specification Language and therefore can be processed by tools. It would be helpful to have a website where the specifications are available for download.

To conclude, the book is well written and carefully motivated. The book provides useful literature surveys in the bibliographical at the end of each chapter. There is a helpful notational index, as well as a concept index. The number of cross references within the book is impressive. All the material is technically correct with surprisingly few errors. The material is presented with numerous exercises that serve for the further development of the theory; and the further material often depends in these exercises (although hints are given in these cases). Altogether, this book is an important compendium in the field of axiomatic specifications.

This is an important book. It is big and ambitious, but some things must be done carefully, or they can't be done at all. Building a big software system is one such thing. Describing a method how to build a big software system is another such thing. Writing a book about the foundations of the methods to build big software systems is yet another such thing. Reading such a book also requires some care and ambition. But if you want to learn how to build big software systems, and to know what you are doing while you are doing it, then you are already quite ambitious. I think that this book can help. I read most of it although I don't work in software specifications any more. It would have been easier if I had it in the time when I worked in the area.

It would be nice if Amazon could get a more reasonable discount from the publisher Springer, so that more students can get the book.