Algebraic Specification of Abstract Data Types

We have seen that the role of the DEFINITION MODULE in Modula-2 is to provide users with information on the type(s) and operations available to them. The operations specified in the DEFINITION MODULE are available to users of the abstract data type and allow them to manipulate values of the data type in any application program. However, it is these and only these operations, as stated in the DEFINITION MODULE which are available to the user. The representation of the abstract data type and the implementation of the operations are explicitly programmed in the corresponding IMPLEMENTATION MODULE by the implementor of the abstract data type which is hidden from the user.

In contrast, for an algebraic specification of an abstract data type, there is no implementation - the algebraic specification provides a complete mathematical description of both the syntax and semantics of an abstract data type. Hence, in a sense, the implementation is now shielded not only from the user but from everyone !

The virtue of the algebraic approach to specification is that unlike its Modula-2 and Ada analogues, it also provides a means for specifying the semantics of an abstract data type in a formal manner. This is achieved by the use of equations or axioms which express relations between the operations in terms of compositions (applications) of two (or more) corresponding functions. Let us now examine the structure of an algebraic specification. An algebraic specification of an abstract data type provides a user with

• the name of the abstract data type

• a collection of sorts, corresponding to the sets of objects (abstract data values) which are manipulated by the operations of the abstract data type

• a collection of operations together with their signatures which provides the syntactic component of the specification of the abstract data type

• a set of equations or axioms which relate the operations and which provides a formal description of their behaviour (the semantics) of the abstract data type.

In the algebraic approach, the operations of an abstract data type are implicitly defined in terms of a set of axioms or equations, each of which relates two or more of the operations. The operations are therefore defined implicitly by relating their meanings to each other and there is no concept of a ``state'' or ``model'' as in VDM. These ideas will be explored shortly when we develop an algebraic specification for an unbounded stack of natural numbers.