DISI Dipartimento di Informatica e Scienze dell'Informazione

Basic Concepts

Chapter 1 of
Algebraic System Specification and Development: Survey and Annotated Bibliography. 2nd edition, 1997
M. Cerioli .
In Algebraic System Specification and Development: Survey and Annotated Bibliography. 2nd edition, 1997, number 3 in Monographs of the Bremen Institute of Safe Systems, chapter 1. Shaker, 1998.
Excerpts from Preface and Introduction
Methods for the algebraic specification of abstract data types were proposed in the early seventies in the USA and Canada and became a major research issue in Europe shortly afterwards. Since then the algebraic approach has come to play a central role in research on formal program specification and development, as its range of applications was extended to the specification of complete software systems, to the formal description of the program development process, and to the uniform definition of syntax and semantics of programming languages. Today this approach extends beyond just software to the development of integrated hardware and software systems. These flourishing activities in the area of algebraic specifications have led to an abundance of approaches, theories and concepts, which have universal algebra, category theory and logic as a common mathematical basis.

The present volume is an annotated bibliography which attempts to provide an up-to-date overview of past and present work on algebraic specification. No attempt is made to provide a coherent introduction to the topic for beginners; the intention is rather to provide a guide to the current literature for researchers in algebraic specification and neighbouring fields. Some indications of how the different approaches are related are included.

Chapter 1: Basic Concepts
A discussion which arose early in the history of work on algebraic specifications concerned the choice of semantics of a specification. In the context of purely equational (or conditional equational) specifications, the obvious choice of taking the class of all algebras which are models of the axioms is ruled out since this will always admit undesirable trivial models. An early suggestion was to restrict attention to the initial object(s) in this category of models; another possibility is to restrict attention to the terminal object(s) in a certain sub-category of models; other choices are also possible.

Any approach to algebraic specification must be based on some notion of algebra and some choice of logical system in which to write axioms. Early approaches were based on many-sorted algebras and equational axioms. Soon it became clear that this is not always flexible enough. Some data types and functions can only be described in an awkward fashion using equational logic, and there are some cases where equations are not powerful enough. It is apparent that more complicated logical systems and more complicated notions of algebra are needed to cope with ``awkward'' aspects of programs such as: types, partial and non-strict functions; higher-order functions and infinite objects; non-deterministic functions and concurrent systems. A great deal of work has been devoted to enriching the basic algebraic specification framework to deal with these complications. It turns out that much of the work on algebraic specifications that has been done is actually independent of the notion of algebra and the logic used to write axioms: it is possible to formulate many results in the context of an arbitrary institution.