Fundamentals of Algebraic Specification 1

The theory of algebraic specifications has its origins in the mid seventies and evolved from different sources and work independently done by different authors. Conceptually it is based on notions and ideas of classical and universal algebra in pure mathematics, and on concepts of abstract data types and software system specification in computer science.

Equational axioms like associativity and commutativity are well-known from arithmetic in natural numbers IN, integers II, reals IR and most other number systems.

In the last chapter we have introduced algebraic specifications and algebras satisfying the given equations. In general there are many different algebras for each specification SPEC. In this chapter we want to consider a distinguished algebra, the quotient term algebra T _SPEC, which is generated by its operations and satisfies some ground equations E if and only if E is valid in all SPEC-algebras. The last property is called “typical”. In Chapter 3 we will see that these properties “generated” and “typical” are characterizing T_SPEC uniquely up to isomorphism of algebras.

We study in this chapter initial semantics of equational specifications. In contrast to the former, mainly introductory chapter we will now emphazise the algebraic fundamentals of initial semantics and discuss in more general terms the concepts of quotient term algebras and initiality. These algebraic fundamentals are of great importance since they enable us to develop a theory of data type specification with initial algebra semantics, which not only yields a deeper understanding of initial semantics, but also exhibits results which are of extrordinary help in the practice of specification.

We have seen in chapters 2 and 3 that a specification SPEC defines the class Alg(SPEC) of algebras for that specification. We have been able to single out a specific isomorphism class of algebras, the initial algebras, which due to their properties of being generated and typical can serve as favorite candidates for semantics of specification. That we could do so, is intrinsically a property of equations which we used as axioms in specifications. One could think of axioms other than equations, and allow Horn-clauses or even arbitrary first order formulas. It is indeed not obvious that initial algebras exist as models of a specification, and it is even possible to show that with arbitrary first order formulas as axioms aninitial algebra in the defined class of models not always exists.

The formalism of algebraic specifications allows to specify data types and software systems independent from their representation and without reference to any particular machine configuration or operating system available. They are,with respect to semantics,independent from technological changes (other than most programming languages for example) and build a reliable basis for documentation and implementation. Indeed, the fact that we can write specifications and know about their meaning is a great achievement, but it is only part of what algebraic specifications do provide: They may be viewed as an axiomatization of the theory of the data type they specify. In this respect they admit formal theorem proving and give rise to automatization of correctness and validation of formal properties. On the other hand they can be considered as input of an interpreter which formally evaluates terms thus producing normal form terms which may be serving as representations of data. These two aspects are the reason that we discuss in this chapter the equational calculus for proving equations from specifications, and the term rewriting with equations for deriving terms from terms. Actually the equational calculus and term rewriting with equations are closely related, and we will see that they can simulate each other.

This chapter deals with the question of how to prove that a specification is correct w.r.t. a given data type. Since correctness proofs are usually a lengthy and nontrivial task, but are of extraordinary importance if one wants to rely on the specification, it is natural to ask for techniques and tools which can guide and support the work of performing the proof. In general, a correctness proof can never be fully automatized since there are usually different objects to compare: specifications and algebras. The algebra to which a specification is related, however, must be given in some mathematical terminology, since otherwise it is impossible to formulate a correctness proof at all. Since correctness is in general a recursively undecidable predicate it remains the duty of the specifier to perform the correctness proof in most cases. On the other hand, there are usually parts in a correctness proof which allow for an automatization. We have abstained to discuss in this volume the criteria of correctness which can be tested by a theorem prover though much work has been done in this direction. Instead, we have emphasized on the “semantical” conditions for correctness and we will try in this chapter to expose some of the experience in designing specifications and in correctness proofs. This “pragmatic” component of algebraic specification of abstract data types has rarely been discussed in the literature, but is certainly of major importance for the application of algebraic specifications.

There are several examples of abstract data types in Computer Science, like strings, stacks and binary trees, which are used in slightly different versions in a number of different applications.

In the last chapter we have introduced parameterized specifications, like string(data), in order to replace a family of similar specifications, like string(nat) for strings of natural numbers, string(int) for strings of integers and string(spec) for strings over some other specification spec, by only one specification including a designated formal parameter specification. Moreover we have mentioned that parameterized specifications are most useful in order to obtain modularity of larger specifications and to allow reusability of the corresponding subspecifications.

For the specification of basic abstract data types as considered in Chapter 2 and for the parameterized case in Chapter 7 it is usually sufficient to give the specifications explicitly as a triple SPEC = (S,OP,E) of sorts S, constant and operation symbols OP, and equations E. For the specification of software systems, however, it would be problematic to give a specification explicitly in terms of large sets S, OP and E, because it is difficult to write, read and understand those large “flat specifications”. According to the principles of software development large systems should be subdivided into smaller subsystems. In the same way the specification of a large system should be subdivided into smaller subspecifications. On the other hand there must be concepts to build up larger specifications from smaller parts. This is the essential aim of a specification language. In this chapter we will introduce five concepts of a specification language which are based on a number of constructions on specifications studied in previous chapters of this book.

In this chapter we present the semantics of the algebraic specification language ACT ONE which was introduced in the last chapter. The semantics is defined formally on two levels: The first level is that of parameterized specifications and the second that of free functors associated with parameterized specifications in the sense of Chapter 7. Given an ACT ONE definition we define in the first level the corresponding parameterized specifications PSPEC = (FSPEC,TSPEC), where FSPEC is the formal parameter and TSPEC the target specification. Note that, although PSPEC was viewed as a syntactical object in Chapters 7 and 8, is it now the first level of semantics of an ACT ONE definition. The definition has now to be considered as the syntactical level. The semantics of PSPEC in the sense of Chapter 7 are all free functors F:Cat(FSPEC) → Cat(TSPEC). In this chapter we represent the semantics by only one free functor F because all other ones are natural isomorphic to F. Since PSPEC = (FSPEC,TSPEC) was already the first level of semantics w.r.t. the given ACT ONE definition, the parameterized data type PDAT = (FSPEC,TSPEC,F) is the second level of semantics w.r.t. the ACT ONE definition.