Specification of Abstract Data Types

In the early days, the computer scientist was very much pre-occupied with machine-oriented problems of storage and data representation - concrete details. The realisation that data types are not simply a set of values but consist also of a collection of operations which act upon the values led to an awareness of the importance of data abstraction for both programming language design and the specification of software systems. In particular, the importance of separating the specification of an abstract data type from its representation has long been recognised with the resulting benefits for the modularisation of software, software reusability and data integrity. This concept is supported by a number of programming languages including Ada and Modula-2. In the case of Modula-2, a definition module provides information about the syntax of an abstract data type while the representation of the data type and the implementation of its associated operations are provided by a corresponding implementation module. The corresponding structures in Ada are provided by the package header (specification) and package body respectively.

As an illustration, consider the specification of an unbounded stack. The stack is an example of a LIFO (last-in-first-out) structure which has many applications in computer science. Yet it is important to realise that the characteristic behaviour of a stack is quite independent of the data it manipulates or the representation of the stack itself. It is the collection of operations which can be performed upon a stack that defines its behaviour. In particular, data values can be pushed onto the top of a stack or popped and retrieved from the top of a non-empty stack so that the behaviour of a stack can be described in terms of the following operations :

• init :     an operation which creates an initial empty stack.
• push :     an operation which adds a data element to the top of an existing stack to produce a new stack.
• pop :     an operation which takes a stack as input and produces a new stack with the top-most element removed.
• top :     an operation which takes a stack as input and returns the element at the top of the stack.
• isempty :     an operation which takes a stack as input and returns true if the stack is empty, false otherwise.

As a prelude to the development of an algebraic specification for the stack, it will be instructive to look briefly at how such an abstract data type might be specified in a high-level imperative language such as Modula-2. This will serve not only to introduce some basic terminology and notation which will be used in the subsequent discussion on algebraic specifications, but will also help to put the algebraic approach into sharper perspective. Those not familiar with Modula-2, but with a working knowledge of any procedural language such as Fortran, Pascal or C will find no difficulty in understanding the specification.

With Modula-2, the user of an abstract data type is presented with a signature in the form of a DEFINITION MODULE which specifies the syntax of the components of an abstract data type by means of formal Modula-2 declarations (such as TYPE and PROCEDURE statements). The DEFINITION MODULE presents an external interface to users of the abstract data type and so must provide a clear and precise description of the resources available. In other words, the DEFINITION MODULE must adequately describe ``what the abstract data type does''. For a stack of natural numbers (non-negative integers corresponding to the pre-defined data type CARDINAL in Modula-2) with the operations described above, the DEFINITION MODULE is given in Fig. 8.1.

  

Figure 8.1: Modula-2 signature for an unbounded stack

The following points should be noted :

• The representation of the abstract data type Stacks and the implementation of the operations are contained in a corresponding IMPLEMENTATION MODULE, the details of which are hidden from the user and this module is the exclusive responsibility of the implementor of the abstract data type. Users can only access and manipulate the data items by means of the operations provided in the DEFINITION MODULE.
• The data type and its operations can be exported which means that other modules can declare variables of that type and modify them using the exported operations.
• The operations are expressed in terms of function procedures, subprograms which return a single result. The type identifier following the final semicolon states the type of the result returned for each function. The reason for using functions to provide all the operations of the abstract data type will be explained shortly.
• Note that the function init() : Stack must be used to create an initially empty stack for each required instance of a stack. Here, it is a function without arguments and so essentially represents a constant value of type Stack. Such ``constant'' operations (functions) are known as nullary operations.
• One implication of using functions to provide all the operations is that the traditional ``pop'' operation which removes the top-most element from a stack and returns the value of that top-most element has been separated into two distinct operations. The function pop simply returns the truncated stack while top returns the value of the top-most element of the stack.
• The identifier Stack, following the reserved word TYPE, declares that the data type Stack is opaque. The implementation of such types is hidden from its users and resides in the corresponding IMPLEMENTATION MODULE where the full details of its representation and implementation are given.
• The package specification and package body of Ada are similar to the DEFINITION MODULE and IMPLEMENTATION MODULE of Modula-2 with the access private type of Ada being equivalent to the opaque type of Modula-2.