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.