<figure><img src="image_1.png" /></figure>

HAL
open science

# Algebraic specification of abstract data types

Marie-Claude Gaudel

► To cite this version:

Marie-Claude Gaudel. Algebraic specification of abstract data types. [Research Report] IRIA-RR-360, IRIA. 1979, pp.31. hal-04716600

HAL Id: hal-04716600

https://inria.hal.science/hal-04716600v1

Submitted on 1 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Inv. 07441 RR360

RIA

laboria

ARCHIVES

laboratoire de recherche
en informatique
et automatique

<figure><img src="image_3.png" /></figure>

ALGEBRAIC SPECIFICATION
OF ABSTRACT DATA TYPES

Marie-Claude GAUDEL

31p.

Rapport de Recherche N° 360

Août 1979

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20
ALGEBRAIC SPECIFICATION OF ABSTRACT DATA TYPES

Marie-Claude Gaudel

Résumé :

Ce rapport est une introduction à l'étude des types abstraits algébriques. Les principaux résultats dans ce domaine sont présentés et commentés.

Abstracts :

This report is a survey of the properties of algebraic abstract data types. The main results in this area are pointed out and discussed.

N.B. Ce texte a été rédigé à l'occasion du 2ème cours avancé sur la Sûreté de Fonctionnement des Systèmes.

N.B. This paper has been prepared for the 2nd advanced course on Computing Systems Reliability, September 10, 21 1979, Toulouse (France).
## Introduction :

Many possible approaches to the specification of abstract data types are being currently developped. The algebraic approach provides a formal way of describing properties of the values and operations of an abstract data type. This abstract definition is independent of any particular implementation. It makes it possible to reason about programs using such data types and to prove implementations. In this talk the following points are introduced :

I) Definitions and Examples,

II) Problems of Completeness and Consistency,

III) Specification of Error Cases,

IV) Correctness Proofs of Representation.
# I) Definitions and Examples

## I.1 Informal Introduction

It seems now to be generally accepted [BG 77, GH 78, GTW 78] that an abstract data type can be considered as a many-sorted algebraic theory which is given by a "presentation", including :

- a set of sort names;

- a signature, i.e a set of operation names with their corresponding arity (the names of domains and co-domain). These symbols are used to write the "terms" of the abstract data type;

- a set of axioms (or laws) which express the relationship between the operations. These axioms are equations between terms composed of operations and free variables. These variables are implicitly universally quantified over their corresponding sort.

**Example 1** : As a first example, let us consider a presentation of the boolean type :

type Bool ;

operations

( ) → Bool : true, false ;

(Bool) → Bool : ⊢ ;

(Bool, Bool) → Bool : ∧, ∨, ⊢, eq ;

axioms

declare b, b' ∈ Bool ;

∃ true = false ;

∃∃ b = b ;

∧ (true, b) = b ;

∧ (false, b) = false ;

∧ (b, b') = ∧ (b', b) ;

∨ (b, b') = ∧ (∃b, ∃b') ;
```pascal
> (b, b') = v (¬b, b');
eq(b, b') = ∧ (>(b,b'), >(b', b))
(1)
end
```

From this example, one can see that the **operations** part of the presentation defines a language : the language of terms of the Bool data type (which is also called the "word algebra" of Bool). The **axioms** part of the presentation defines one (or more) congruence relations on these terms. If there is no **axioms**, all the terms of the abstract data type are different.

In the general case, when there are some **axioms**, they define some **equivalence classes** in the language of terms.

A second, well-known, example is the "Set of Integers" data type, [HOA 72, GH 78]. The Integer type is supposed to be predefined and the operations to be specified are : to insert or delete an integer in a set or to test if an integer belongs to a set. A presentation of this data type can be written :

**Example 2 :**

```pascal
type Set, Bool, Int;
```

**operations**

( ) → Set : empty-set;
(Set, Int) → Set : insert, delete;
(Set, Int) → Bool : member-of ? ;

**axioms**

```pascal
declare s∈Set, i,i'∈Int;
member-of ?(empty-set) = false;
member-of ?(insert(s,i),i') = if ?=(i,i') then true
                                else member-of ? (s,i');
```

<footnote>(1) In the rest of the paper the binary operators of this data type are used in an infixed way, with the usual conventions for priority. Furthermore, formulae such that $p=true$ will be written 'p' when this is not confusing.</footnote>
```pascal
delete empty-set,i) = empty-set;
delete (insert(s,i),i') = if ?=? (i,i') then delete(s,i')
                          else insert(delete(s,i'),i);
end
```

In this presentation some conditional equations occur. As it is mentioned in [GTW 78], it is possible to enrich every data type T with an "if-then-else" operation by adding to the axioms of T the following equations :

```
if-then-else(true,t,t') = t
if-then-else(false,t,t') = t'.
```

Thus, it is possible to write conditional equations without departing from the framework of standard algebra. These equations play a very important role in algebraic specification, since they make it possible to write a recursive definition of operations.

While the first three axioms in example 2 are simple (recursive or not) definitions, the last one may seem less readable to people who are not familiar with algebraic specifications. In order to clarify the meaning of this definition, let us consider the following term :

```
delete insert (insert (insert (empty-set, 2), 3), 2), 2)
```

Using the last axiom in a repetitive way, one can see that this term is equal to :

```
= delete (insert (insert (empty-set, 2), 3), 2)
(since it is the case where i ?=? i')
= insert (delete (insert (empty-set, 2), 2), 3)
= insert (empty-set, 3)
```

which is the intended result.

It is interesting to compare [GH 78] this data type and that obtained by changing this axiom into :

```
delete (insert(s,i),i') = if ?=? (i,i') then s
                          else insert(delete(s,i'),i).
```

The new data type is rather different and is the so-called "Bag" data type or "Multiset" which is nothing more than a counted set. Notice that, for the data type Set, the following theorem holds :

```
member-of? (delete(s,i),i) = false
```
Some authors [GH 78, GHM 78, BG 77] single out one name of sort which is
often called the T.O.I. (type of interest) : in example 2 the T.O.I. is
Set. Then one can see immediatly in a specification which data type is
defined, which ones are used and considered as predefined etc... (2)

In order to conclude this informal introduction, we shall point out that
the presentation of an algebraic abstract data type has a relatively simple
syntax. The base language has three primitives :

. functional composition ;

. the sign = ;

. an unbounded supply of free variables.

Moreover the Bool data type (as given in example 1) is used and an "if-then-
else" operation is assumed for every data type.

But, if the syntax of such presentations is elementary, their semantics is
less obvious and needs to be studied carefully. This will be done in the
two next parts of this paper.

I.2 - Initial Algebras

We give here very briefly some fundamental definitions and results taken
out of [GTW 78], in order to define in a formal way what is the data type
specified by a presentation.

Let us consider a signature Σ (i.e a set of operation names with their
arities). T<sub>Σ</sub> is the set of terms one can write using symbols of Σ.

A Σ-algebra A, is a many-sorted algebra such that : to each name of sort, s,
occuring in Σ corresponds a carrier A<sub>s</sub> of this algebra ; to each name of
operation of Σ corresponds an operation σ<sub>A</sub> of A.

As an example, we call Σ<sub>b</sub> the list of operations of the Boolean data type,
as given in example 1. In this case, the Σ<sub>b</sub>-algebras are homogeneous since
there is only one name of sort : Bool.

<footnote>(2) One of the (highly valuable) ideas in [BG 77] is to provide a specifica-
tion language to define data types in a modular and structured way.</footnote>
Then we can give two examples of $\Sigma_b$-algebras :

**Example 1.1 :**

Given the set $A_b = T_{\Sigma_b}$, we can consider the operations true, false, $\neg$, $\wedge$, ...
as operations on $A_b$ which compute terms of type Bool.
Thus $T_{\Sigma_b}$ can be considered as a $\Sigma_b$-algebra.

**Example 1.2 :**

Now we consider the set $A'_b = \{\text{true, false}\}$ and the usual operations on
booleans denoted true, false, $\neg$, $\wedge$, ... This is also a $\Sigma_b$-algebra.

Notice that, whatever $\Sigma$ is, it is always possible to consider $T_\Sigma$ as a
$\Sigma$-algebra. Moreover, it is a well-known result that $T_\Sigma$ is an initial algebra
in the class of $\Sigma$-algebras, i.e there is a unique $\Sigma$-homomorphism$^{(3)}$ from
$T_\Sigma$ to every $\Sigma$-algebra.

Now, let us associate to the signature $\Sigma$ a set $E$ of $\Sigma$-equations (a $\Sigma$-equation is an equation composed of symbols of $\Sigma$ and free variables). Among the congruence relations on $T_\Sigma$ which are compatible with $E$, we call $\equiv_E$ the smallest one$^{(4)}$.

We denote $T_\Sigma / \equiv_E$ the $\Sigma$-algebra *quotient* of $T_\Sigma$ by $\equiv_E$: in $T_\Sigma / \equiv_E$ the operations of $\Sigma$ are defined no more on the terms, but on the equivalence classes of terms defined by $\equiv_E$. It can be proved that it is a $\Sigma$-algebra and that it is initial in the class of all $\Sigma$-algebras satisfying $E$.

Following the definition given in [GTW 78], the abstract data type defined
by a presentation <Σ,E> is this initial algebra, which is denoted T<sub>Σ,E</sub>.

If one wishes to forget, as far as possible, the mathematical vocabulary,
the meaning of this definition is : the values (or the objects) of an
abstract data type are equivalence classes of terms ; the equivalence

(3) A $\Sigma$-homomorphism from A to B is a class h of functions which preserves the operations of $\Sigma$, i.e :

$$
h(\sigma_A(x)) = \sigma_B(h(x))
$$

(4) Intuitively, it means that a couple $(t, t')$ verifies $\equiv_E$ only if $t \equiv_E t'$ is a consequence of $E$.
relation considered is minimal, i.e the equations of E are satisfied, no more.

Coming back to our example Bool, let us call $E_b$ the set of equations given in example 1. $E_b$ defines two equivalence classes : T is the set of terms which can be proved equal to true, F is the set of those which are equal to false. Operations $\neg$, $^$, ..., are defined on these two equivalence classes, and from $E_b$, we have :

$$ \neg T = F $$

$$ \neg\neg T = T \Rightarrow \neg F = T \dots $$

It is possible to define these operations completely and thus to show that $T_{\Sigma_b}, E_b$ is isomorphic to the well-known, well understood algebra of booleans.

In the same time we get a proof that our specification of booleans is correct.

This is the essential result given by this (very) theoretical formulation of abstract data types : a specification $(\Sigma,E)$ is correct if $T_{\Sigma,E}$ is isomorphic with a mathematical model of the data type. However, such a model is not always obvious to produce and very often the problem which preexists to the abstract data type is a computer science oriented one (see [GDH 78] for instance). In this case such a formalism may seem less necessary and less mathematical notations with practical methodologies to write correct specifications are probably sufficient.

## I.3 - Data type Induction

A useful method for verifying, at least partially, a data type specification is to prove the intended properties of the data type from its specification.

A soon as this specification is independant from any representation or environment, the proofs are generally simple and use the same general principle [SW 75, GHM 76, WS 76] :

Let us consider a data type T, where $f_1, \dots, f_n$ are the operations of the data type with result of type T. Let P(x) be a property of values of T. Suppose that, for all i=1, ..., n, if P is true for all the operands of $f_i$ of type T, P is true for the result of $f_i$. Then P is true for all values of T.
This proof technique, called by "data type induction" or by "generator induction", can be used when the data type is protected: the user of the type knows only the names and the characteristics of the operations and have no ideas of the way they are realized.

Here the properties of the operations are given by algebraic axioms, in other specification methods Pre-and Post-conditions are used or definitions in terms of sequences, etc. But the proof technique remains the same.

**Example 2.1 :**

Suppose the following property of the data type `Set` has to be proved :

∀s∈Set, ∃i∈Int, member-of? (delete(s,i),i) = false.

Operations whose co-domain is Set are : empty-set, insert, delete.
We start the proof by giving a Lemma.

**Normal Form Lemma :** let

$P(s)=(s=\text{empty-set}) \lor (\exists s_1 \in \text{Set}, i \in \text{Int } s.t.s=\text{insert}(s_1, i_1) \land P(s_1))=\text{true})$
then $\forall s \in \text{Set}, P(s)=\text{true}$.

a) $s$ = empty-set implies $P(s)$ = true ;

b) $s$ = insert($s'$,i) with $P(s')$ = true, implies $P(s)$ = true ;

c) $s$ = delete($s'$,i) with $P(s')$ = true, either :

- $s'$ = empty-set implies, from the third axiom, that

$s$ = empty-set, thus $P(s)$ = true ; or :

- ∃s₁ ∈ Set, i₁ ∈ Int such that s' = insert (s₁, i).

from the last axiom

$s=\underset{i ?=?}{\text{if}} i_1 \underset{\text{then}}{\text{delete}}(s_1,i) \underset{\text{else}}{\text{insert}}(\text{delete}(s_1,i),i_1)$

In the else-case it is straightforward that P(s)=true and in the then-case
it comes by induction. □

We can now give a proof for the property given below :

a) $s$ = empty-set

`∀i∈Int member-of?(delete empty-set,i),i=member-of?(empty-set,i)=false ;`

b) $s$ = insert($s'$,i') with

`∀i∈int member-of?(delete(s',i),i)=false`
then

member-of?(delete insert(s',i'),i) =

member-of?(if i ?=? i' then delete(s',i) else insert(delete(s',i),i'),i) =
putting out the conditional (a so-called case analysis), we get

if i ?=? i'

member-of?(delete(s',i),i)=false (by induction hypothesis)

if i ?=? i' is false

member-of?(insert(delete(s',i),i'),i) =

if i ?=? i' then true else member-of?(delete(s',i),i) =
member-of?(delete(s',i),i) = false

c) s = delete(s',j)

The normal form lemma makes it possible to reduce this case to case a) or b). □

## II) Problems of Consistency and Completeness

While it is rather simple to reason about a given algebraic abstract data type, it is quite more difficult to design a specification for such a data type and to answer the following questions : has one supplied a sufficient number of axioms to define the data type ? do the axioms introduce some contradictions ? An example of inconsistency would be the possibility in example 2 to find a "s" and a "i" such that

member-of?(s,i) = true

and

member-of?(s,i) = false

could be deduced from the axioms.

It has been seen that, if a mathematical model preexists to the design of the specification, a verification method it to construct a model for the specification and to prove it isomorphic to the first one.

If such a model does not preexist, the consistency and the completeness of the axioms must be directly checked up. These two problems are, in general, indecidable.
The consistency can be proved by treating the axioms as left to right
rewrite rules and demonstrating that they exhibit the Church-Rosser
property : i.e, whenever one applies a rewrite rule to reduce a term,
and a rule to reduce the resulting term, etc, until there is no longer
an applicable rule, the final result is independent of the order in
which the rules are applied. A useful method for verifying this property
is presented in [KB 70].

The notion of completeness, in the framework of algebraic abstract data type, has to be looked at carefully. In mathematics, a theory, or the set of axioms which define it, is complete if it is consistent and if every formula in it is decidable [Sch 67]. It implies that every equality between terms can be proved either true or false.

Example 2 does not satisfy this property, since the following equality :

insert insert(s,i),i' ) = insert insert(s,i'),i)

can be stated neither true nor false, using the given axioms (5). However
this specification of the "Set of Integer" data type satisfyies the
informal definition of it given in I.1 : the properties of the "insett",
"delete" and "member-of?" operations has been sufficiently defined ;
equality between terms of data type Set is not necessary here.

Gutttag and Horning in [GH 78] state a specific notion of completeness
for algebraic abstract data type : the so-called sufficient completeness.
We now present very briefly the main definitions and results of [GH 78].

Definition 1 :

Given a presentation <T,F,A> of an algebraic abstract data type, where t∈T
is the T.O.I, the set of operations F can be partitionned into two sets

(5) Remind that if the abstract data type is considered as the T<sub>E,E</sub>
initial algebra, these two terms are, by definition, different.
It will appear, when studying representation proofs, that it may
be interesting to leave the answer unspecified.
S and O, such that S contains exactly those operations whose range is t,
and O the other ones. (Operations in O have at least one operand of type t).

The intuitive definition of sufficient completeness is that A is a suffi-
ciently complete axiomatization of t if every term of <T,S+O,A>, which
begins by an operation of O, can be rewritten, using A, as an "external
term". An external term is a term which contains no operations of S+O,
for instance a constant of a data type tᵢ of T such that tᵢ ≠ t.

In example 2, there is :

T = {Set, Int, Bool}
S = {empty-set, insert, delete}
O = {member-of?}
t = Set

In this case sufficient completeness is verified by demonstrating that for
every s in Set, every i in Int, the term :

member-of?(s,i)

can be proved equal to either true or false. The proof can be done by data
type induction, using the fact (proved in I.2) that every term of type Set
can be rewritten as "empty set" or "insert(s,i)".

The formal definition of sufficient completeness is a bit complicated
since the notion of external term has to be precisely stated. Let us call
I the list T-{t} of names of types which are not the T.O.I.

We note T_I the set of terms, of type t_i ∈ I, where operations of S+O do not occur, i.e the terms of predefined data types.

**Definition 2 :**

For any abstract data type presentation <t+I,S+O,A>, A is a _sufficiently-complete axiomatization_ of the data type if and only if, for every term of the form f_i(x_1,...,x_n) where f_i ∈ O, there exists a theorem derivable from A of the form f_i(x_1,..., x_n)=u where u ∈ t_j and u ∈ T_I. A is consistent if for each f_i(x_1,..., x_n) u is unique (up to equality on t_j).

It can be shown that the problem of establishing whether or not a set of
axioms is sufficiently-complete is, in general, indecidable. However, if
some limitations on the kinds of axiomatizations specified are accepted, it is possible to state conditions that are sufficient to ensure sufficient-completeness.

In order to give an idea of these limitations, we need to give a few definitions and to introduce some notations.

Axioms will be noted in the following way :

$$f(x^*)=z$$

where f is an operation name, $x^*$ a list of free variables or of expressions $g(y^*)$. z has the same syntax but one or more conditionals can occur.

**Definition 3 :**

NEST(x) is equal to the greatest depth to which operations contained in S+O are nested in the expression x. An axiom, $f(x^*)=z$, is _monotone in NEST_ (m(NEST)) if

$$NEST(f(x^*))>NEST(z).$$

Operations in S which have no operands of type t are called _constants_ of t. For instance "empty-set" is a constant of the Set data type. We consider that, in every data type, there is at least such an operation, and at least one operation in O : constants are obviously necessary to write terms of type t ; a type for which O is empty would be quite uninteresting since there would be no way to express the properties of its values.

**Definition 4 :**

A is a _safe_ axiomatization of <T,S+O,A> if $\forall o \in O$ and $\forall s \in S$ there exists an axiom of the form

$$o(s(x^*),y^*)=z$$

(where $x^*$ and $y^*$ are two free variables lists), verifying either :

(I) z contains no conditionals and either the axiom is m(NEST), or there exists a theorem $z=z'$, derivable from A, such that $o(s(x^*),y^*)=z'$ is m(NEST) ; or
(II) z is of the form if b then z1 else z2 where o(s(x*),y*)=z1 and o(s(x*),y*)=z2 satisfy (I) and NEST(b)<NEST(o(s(x*),y*)) or there exists a theorem b=b' derivable from A, such that o(s(x*),y*)=z' is m(NEST) ; or :

(III) z is of the form if b then z1 else z2 where o(s(x*),y*)=z1 and o(s(x*),y*)=z2 satisfy one of the properties (I), (II), (III) and NEST(b)<NEST(o(s(x*),y*)) or there exists a theorem b=b' such that NEST(b')<NEST(o(s(x*),y*)).

The recursivity of property III makes it possible to deal with nested
conditionals. Property I and II are the basis of the induction.

The motivation of this definition is that one wants to eliminate the
operations of S+O from every term beginning by an O operation, using the
axioms as rewrite rules. If A is safe, it is straightforward that it is
sufficiently complete.

Most of the usual axiomatizations are not safe. For instance the axioma-
tization of example 2 is not safe since there is no axioms with, as left-
hand side :

`member-of?(delete(s,i),j)`

However, this axiomatization is sufficiently complete.

Indeed, it has been proved that every term of the form "delete(s,i)"
can be rewrite using only "empty-set" and "insert". Hence the notion of
convertible operations which is stated now :

**Definition 5 :**

Given a presentation <T,S+O+{f},A> where the arity of f is
t×t<sub>i|</sub> ×...×t<sub>in</sub> →t, if for each expression f(u,v*) there exists a theorem
derivable from A of the form f(u,v*)=z where z contains no instances of f,
then f is said *convertible* to S.
**Theorem 6:**

A is sufficiently-complete if there exists a partitioning of S into disjoint sets C(con constructing) and E(extensions) such that all constants are contained in C and

1) For all $c \in C$ and all $o \in O$ there exists an axiom $o(c(x^*), y^*)=z$ satisfying the properties of definition 4 and

2) There exists an ordering $e_1, e_2, \dots, e_m$, of the functions in E such that $e_1$ is convertible to C, $e_2$ is convertible to $C+\{e_2\}$, etc.

This theorem provides a purely syntactic method of verifying sufficient-completeness of a large class of abstract data types. It is shown in [GH 78] that for any type all of whose operations are primitive recursive, either there exists an axiomatization A verifying Theorem 6, or it is possible to get one, adding some auxiliary functions to S or O.

Furthermore, theorem 6 leads to a methodology to design sufficiently-complete axiomatizations: first, partition the operations into the sets C, O, E; then build the set of left-hand sides $o(c(x^*), y^*)$ and, using only operations from C+O write the associated right-hand sides in such a way that the properties of Definition 4 are satisfied; complete the axiomatization by adding axioms that demonstrate the convertibility of all operations of E.
### III) Error Specification

Error specification is essential in abstract data type definition. It needs to be as formal and precise as the rest of the specification.

Two approaches are presented here : the "restriction specification" used by Guttag in [Gu 78] ; the notion of "abstract error" defined by Goguen in [Go 77].

We first show, by way of an example, that the problem of errors in abstract data type is far from being simple, and that dealing with them without care can introduce inconsistencies in the abstract data type.

#### III.1 Example

The two data types studied in part I and II do not contain error cases. It is not true in most of the usual problems : integers overflow, it is meaningless to divide by zero or to access the top of an empty stack, etc. We present here, as an example, the Queue data type : the first element of an empty queue is not defined, then any attempt to use it is an error. Moreover, removing an element from an empty queue is considered as an error, too.

##### Example 3 :

```pascal
type Queue, Bool, Item;
```

##### operations

( ) -> Queue : emptyq ;

(Queue, Item) -> Queue : append ;

(Queue) -> Queue : remove ;

(Queue) -> Item : first ;

(Queue) -> Bool : empty? ;

##### axioms

declare q∈Queue, i∈Item;

remove(append(q,i))=if empty? (q) then emptyq else append remov(q),i;

first(append(q,i))=if empty? (q) then i else first(q);

empty?(emptyq) = true ;

empty?(append(q,i)) = false ;

end
This axiomatization of Queue is not sufficiently complete since neither "first emptyq", nor "remove emptyq" are defined. A natural idea is to
add the following axioms :

$$
\begin{align*}
first(\text{emptyq}) &= \text{undef}_i \\
remove(\text{emptyq}) &= \text{undef}_q
\end{align*}
$$

Unfortunately, these axioms introduce uninteresting terms in the abstract
data type, such that :

$$
q = \text{append}(\text{emptyq}, \text{first}(\text{emptyq}))
$$

which verifies

$$
first(q) = \text{undef}_i ; \text{empty?}(q) = \text{false} ;
$$

Furthermore, it is necessary to define empty? (undef_q) and first (undef_q).
It seems reasonable to state as new axioms that errors propagate, i.e
that any operation on an undef_t yields an undef of the appropriate type :

$$
\begin{align*}
append(undef_q, i) &= undef_q ; \\
append(q, undef_i) &= undef_q ; \\
empty? (undef_q)    &= undef_b ; \\
first (undef_q)     &= undef_i ; \text{ etc.}
\end{align*}
$$

A disastrous consequence of these rules is that they introduce inconsistencies. For instance, from the axioms of example 3, one can derive :

$$
\mathrm{remove}(\mathrm{append}(\mathrm{emptyq}, \mathrm{first}(\mathrm{emptyq}))) = \mathrm{emptyq}
$$

but from the error propagation rules, it comes :

$$
\begin{align*}
\text{remove}(\text{append}(\text{emptyq}, \text{first}(\text{emptyq}))) &= \\
\text{remove}(\text{append}(\text{emptyq}, \text{undef}_i)) &= \\
\text{remove}(\text{undef}_q) = \text{undef}_q
\end{align*}
$$

$$
\text{thus :} \qquad \text{emptyq} = \text{undef}_q
$$

and then

$$
empty? (undef_q) = true
$$

and since

$$
\begin{align*}
\text{undef}_q &= \text{append}(\text{undef}_q, i) \\
\text{empty?}(\text{undef}_q) &= \text{false} \dots
\end{align*}
$$
In fact, the Queue data type is collapsed down to the one element type
`{undef}!`

It is possible to avoid this drawback by redesigning all the axioms with
a test for every operand of the term defined by the axiom, to know if it
is an "undef". Then the problem is solved for the Queue data type, but the
same difficulty arises for the Item and Boolean data types. They have to
be respecified too.

This is quite contradictory to the basic philosophy of data abstraction :
it is unacceptable to be obliged to rewrite the specification of the data
type Item, when defining a "Queue of Item" data type ; moreover the speci-
fication of normal cases should not be made confusing by a lot of tests
on error cases.

It is desirable to keep "normal" axioms unchanged, with error cases specified
apart, and to avoid to increase to much the size of the specification.
Furthermore the predefined data types used in the specification must be
protected, i.e it is possible to enrich them by new terms but not to modify
the relationship between already existing terms. The two approaches we
present now satisfy these criteria.

### III.2 Restriction Specifications

Gutttag in [Gu 78] suggests to add a "restriction part" to the presentation
of an algebraic data type, where errors are specified. There are two kinds
of such specifications : Pre-condition specifications limit the applicability
of the axioms (and, accordingly, the usable terms of the data type) ;
Failure specifications state that any representation is supposed to fail in
the mentioned cases (i.e to stop, to edit an error message, to jump to some
recovery subroutine, etc, depending on the choosen representation).

The following restriction part could be added to example 3 :

#### restrictions

`Pre(removal, q) = !empty?(q);`

`Pre(first, q) = !empty?(q);`

The *Preconditions* characterize the terms that the user can write with the
guarantee that the axioms are satisfied. The user is in charge of checking
or proving the *Preconditions*, and in proofs on the data type, it is consi-
dered as an hypotheses that for any term *g*(*Y*) the precondition (if it
exists) *Pre*(*g*,*Y*) holds.
A user of the Queue data type, with the restrictions above, must verify or
prove that any operand of "remove" or "first" is not empty. For instance,
he could write :

first(append(q,i))
or if not empty?(q) then first(q) else ...

The user is also in charge of deciding and specifying what has to be done if
the precondition is false.

The Failure specification, on the other hand, let these problems to the
implementor of the type. Let us enrich example 3 in defining an upperbound
to the size of the queues. In order to specify this property, we need an
auxiliary operation : "length" and a restriction which specifies that a
failure must occur if the length of a queue is greater than 100. The
complete specification of the Queue data type becomes :

### Example 3.1 :

type Queue, Bool, Int, Item ;

#### operations

( ) → Queue : emptyq ;
(Queue, Item) → Queue : append ;
(Queue) → Queue : remove ;
(Queue) → Item : first ;
(Queue) → Bool : empty? ;
(Queue) → Int : length ;

#### axioms

declare q∈Queue, i∈Item ;
remove(append(q,i))=if empty?(q) then emptyq else append/remov(q),i;
first(append(q,i))=if empty?(q) then i else first(q);
empty?(emptyq) = true ;
empty?(append(q,i)) = false ;
length emptyq = 0 ;
length(append(q,i)) = length(q) + 1 ;

#### restrictions

Pre(remov(q),q) = not empty?(q) ;
Pre(first,q) = not empty?(q) ;
length(q) ≥ 100 = ⇒ Failure (append,q,i) ;

end
The last restriction specifies that any representation of the "append" operation must check the failure condition. The choice of the error treatment is done by the implementor.

A third kind of restriction, *optionnal failures* is suggested in [Gu 78] : an example is :

$$ \underline{\text{Failure}}(\text{append}, q, i) \Rightarrow \text{length}(q) \geq 100 $$

The meaning of this restriction is that, if the operation append is invoked with arguments q and i and fails to terminate normally, then "length(q)≥100" is true. The failure is optionnal if "length(q)≥100" but must not occur if this condition is not true. Optionnal failures are a way to specify to the implementor some minimal requirements (the maximal size of queues must be, at least, 100). On the other hand, normal failure specifications state imperative requirements to the implementor (the maximal size of queues is 100).

Among the advantages of this method are its simplicity, and the ability to choose at what level of abstraction an error has to be checked and processed : preconditions specify errors of the same level of the data type ; failures can be considered as "abstract" errors, whose conditions only are given, without details of representation.

### III.3 Error-algebras

In I.2, the semantics of a data type presentation has been defined as an initial algebra. If there are errors in the specified data type, Goguen suggests in [Go 77] a similar definition but the considered algebras are specific ones, called error-algebras.

The intuitive ideas are rather simple. As in I.2, the semantics of an abstract data type specified by a presentation is a many-sorted algebra, with, as carrier's elements, equivalence classes of terms defined by the axioms. Among these terms, there are some "errors" (for instance $undef_t$ in III.1). These errors are axiomatized following rules such that : no inconsistencies, error propagation. But this last property is not explicit by the way of axioms : by definition of Error-algebras any operation with an error as operand,yields an error element. It means that there is an infinity of "error-terms" among the terms of the data type, for instance :
undef_q, append empty, first (empty_q)),
remove (emptyq), append (emptyq, undef_i),
empty? (undef_q), not empty? (undef_q), etc.

Some of these terms can be proved equal using the axioms. The corresponding
equivalence classes are error-elements of the error-algebra. Some terms
as "not empty? (undef_q)" or "append (undef_q, i)" cannot be rewritten and define
new error-elements in the carrier of booleans and the carrier of queues.
Thus the indesirable inconsistencies of III.1 are avoided.

The data type Queue presentation becomes :

type Queue, Bool, Int, Item;

operations

( ) -> Queue : emptyq ;

(Queue, Item) -> Queue : append ;

(Queue) -> Item : first ;

(Queue) -> Boolean : empty? ;

(Queue) -> Int : length ;

error-operations

( ) -> Queue : underflow, overflow ;

( ) -> Item : missing ;

axioms

declare q∈Queue, i∈Item;

the same ones as in example 3.1

error-axioms

remove (emptyq) = underflow ;

remove (underflow) = underflow ;

append (overflow, i) = overflow ;

first (emptyq) = missing ;

others

append(q,i)=if length(q)≥100 then overflow else append(q,i) ;

end

Goguen defines the semantics of such a presentation as the initial error-algebra in the category C where : algebras are the class of error-algebras, satisfying the axioms and other properties such that any error axiom has
at least one error-operation, any error-term is interpreted as an error-element; morphims are the so-called error-homomorphisms which preserve errors-elements.

The complete theory needs a rather long presentation and can be found in
[Go 77].

### III.4 Conclusion

It is interesting to compare Goguen's Error-algebras with Guttag's Preconditions: in the first case, all the erroneous terms are introduced in the set of terms of the data type; in the other case, all the erroneous terms are removed from the data type; with error-algebras, the user has to deal with the erroneous terms; using preconditions, he has to check that he does not use them. From a practical point of view, it seems quite similar.

The (optional or not) failure specifications corresponds to a very frequent situation in programming: it is very pleasant to know that a compiler generates the relevant tests on array's indexes. Then it is possible to use array's elements without worrying about index overflow. Generally speaking, failure specifications make it possible to use a term without checking its validity since one knows the implementation will do it. It is especially interesting when one is not interested in a specific error recovery policy. Moreover, it is very useful for the implementor to know which error cases he has to check and which ones has been already checked by the user of the data type. The distinction between preconditions and failures leads to specifications which are, in the same time, more precise for the user and the implementor.
## IV) Correctness proof of representation

It is possible to specify a representation in several ways : with an abstraction function, which takes "concrete" objects and returns abstract objects as results ; with a representation function which associates to any term of the type to be implemented a term of the representing data type.

The first approach has been mentioned first by Hoare in [Hoa 72] and it is more natural if one works with objects (6) of the data type, since one object to be represented can have several representations. This method is used in [GHM 76] and [Gau 78].

The other approach is briefly presented in [GTW 78] and seems more convenient if one is interested in term rewriting or translation problems, as we are [GP 79].

### IV.1 Abstraction function

In all this part, we shall use as example the classical representation of queues by a triplet composed of an array and two integers. The first integer is the subscript of the first queue element, the second one is the subscript of the first free array's element after the queue. In order to simplify the example, the number of elements in the queue and the size of the array are not considered. The specification of the data type Array is given below :

**Example 4 :**

type Array, Int, Item, Bool;

operations

( ) → Array : emptya;

(Array, Int) → Item : access;

(Array, Int, Item) → Array : assign;

(Array, Int) → Bool : def?

<footnote>(6) which have been previously defined [I.1], as equivalence classes of terms.</footnote>
### axioms

declare a beArray, i, j beInt, it beItem;

Note : in order to increase the readability access (a,i) will be noted
a [i].

assign(a,i,it)[j] = if ? = ? (i,j) then it else a[j];

def?(emptya,j) = false ;

def?(assign(a,i,it),j) = if ? = ? (i,j) then true else def?(a,j) ;

### restrictions

¬def? (a,i) ⇒ Failure (access,a,i) ;

### end

The specification of the representation is given by the definition of the
abstraction function A whose arity is :

(Array, Int, Int) → Queue

and which is characterized by the following axioms :

### Example 5 :

emptyq = A(a,i,i) ;

append(A(a,i,j),it) = A(assign(a,j,it),i,j+1) ;

remove(A(a,i,j)) = A(a,i +1,j)

first(A (a,i,j)) = a [i] ;

empty?(A(a,i,j)) = (?(=?(i,j)) ;

A necessary property of this specification is that the new operation A and
the new axioms on it must not introduce inconsistencies in the resulting
data type (for instance representing to different objects by identical
objects).

Thus, consistency and sufficient-completeness must be checked up for the
data type Queue enriched with A.

Moreover other properties must be verified.

Call A the set of (abstract) objects to be represented and C the set of
representing objects. In the example, A is the set of queues and C is the
set of triplets <array, integer, integer>.
<figure><img src="image_4.png" /></figure>

A must be surjective since all the objects in A must be represented. It is not necessarily injective. An object in A can have several representations (for instance the empty queue). Moreover A may not be defined on the whole domain C.

Guttag in [GHM 76] calls the properties which characterize the domain over which A is defined the "representation invariants". In the Queue example, if $<a,i,j>$ belongs to $A^{-1}(A)$ we have :

$i \le j$ and $\forall k$, such that $i \le k < j$, $def?(a,k) = true$

The relation on this domain defined by

$$c \sim c' \Leftrightarrow A(c) = A(c')$$

is called the "equality interpretation".

For instance :

$\forall a, a' \in \text{Array}, \forall i, j \in \text{Int} \quad <a, i, i> \sim <a', j, j>.$

For the representation defined by A to be correct, the properties of the data type to be represented must be preserved in the representing data type : the axioms must be conserved by the representation. Furthermore, ~ must be shown to be an equivalence relation and to be coherent with the operations representation. For instance :

$<a,i,j> \sim <a',i',j'> \Rightarrow \text{remove}(A(<a,i,j>)) = \text{remove}(A(<a',i',j'>))$

In order to express and verify these properties, we now consider not C but the set of equivalence classes of $A^{-1}(A)$ defined by the relation $\sim$. Then a representation is correct if every axiom of the type to be represented becomes
a theorem in $A^{-1}(A)/\sim$, theorem which is derivable from the axioms of the representing types, the representation invariants and the equality interpretation (proved correct).

For instance it is possible to prove that axiom :

first(append(q,it))=if empty?(q) then it else first(q)
is maintained by the representation given in example 5.

The left-hand side becomes :

first(append(A(a,i,j),it)) =
first(A(assign(a,j,it),i,j+1)) =
assign(a,j,it) [i] =
if ?=? (i,j) then it else a [i] ;

The right-hand side becomes :

if ?=? (i,j) then it else first(A(a,i,j)) =
if ?=? (i,j) then it else a [i] ;

Thus, the axiom is verified.

The demonstrations of this sort are not very difficult but rather long.
They are automatable as it has been shown in [GHM 76] and [Mu 77].

IV.2 Representation function

Another way to specify a representation is to associate to every operation
name, f, of the data type to be represented, a derived operation (i.e a
composition of operations) of the representing data types : ρ(f). It must
be done as well for operations with boolean results, thus for equality
which is represented by an equivalence relation ρ(=). ρ(=) is the
equality interpretation mentioned above. ρ can be extended to the terms
and formulae of the represented data type in the classical way :

$$
\hat{\rho}(f(t_1, \dots, t_n)) = \rho(f) (\hat{\rho}(t_1), \dots, \hat{\rho}(t_n))
$$

(ρ and ̂ρ will not be distinguished). If the representing data type is a
cartesian product of several data types, the ith component of ρ(u) is
written ρ_i(u). The specification of the queues representation by triplets
is :
### Example 6 :

```
let ρ(q) = <a,i,j> ;
ρ emptyq = <emptya,o,o> ;
ρ (append(q,it)) = <assign(a,j,it),i,j+1> ;
ρ (remove(q)) = <a,i+1,j> ;
ρ (first(q)) = a [i] ;
ρ (empty?(q)) = (?(=?(i,j))) ;
let ρ(q') = <a',i',j'> ;
ρ (q=q') = (?(=?(j-i,j'-i')) ∧ (o≤k<j-i ≤ ?=(?(a[i+k],a'[i'+k])) ;
```

The equality interpretation is completely specified here : two triplets represent the same queue if the differences between the subscripts (i.e the length of the queues) are equal, and if all the elements are equal. This relation must be an equivalence relation : it is straightforward to verify reflexivity, transitivity and symmetry ; moreover, the representations of equality and of the operations must be, as in IV.1, proved coherent.

For instance

$<a,i,j> ρ(=) <a',i',j'> ⇒ ρ(append)(<a,i,j>, it) ρ(=) ρ(append) (<a',i',j'>, it)$

Furthermore it must be proved that the axioms are kept.

For these proofs, it is necessary to state the representation invariants. It is done by data type induction. Among them, there are :

$$[RI1] ∀q∈Queue ρ_2(q) ≤ ρ_3(q)$$

$$[RI2] ∀q∈Queue, ∀it ∈Item ρ_2(append)(q,it) < ρ_3(append(q,it))$$

### Proof :

[RI1] is true if $q=emptyq$ since

$$ρ(q=emptyq) = (ρ_2(q) = ρ_3(q)) \text{ from } ρ(=) \text{ definition.}$$

Suppose [RI1] verified for $q$. Then it is true for "append(q,it)" since

$$ρ_2(append(q,it)) = ρ_2(q)$$
and $\rho_3(append(q,it)) = \rho_3(q)+1$. Moreover :

$$ \rho_2(append(q,it)) < \rho_3(append(q,it)) $$

i.e [IR2] holds.

[IR1] is also satisfied by "remove(q)" :

$$ \rho_2(\text{remove}(q)) = \rho_2(q)+1 $$

$$ \rho_3(\text{remove}(q)) = \rho_3(q) $$

By induction hypotheses, $\rho_2(q) \le \rho_3(q)$ and from the precondition on "remove", it is assumed that $\neg \text{empty?}(q)$, i.e $\rho_2(q)$ is not equal to $\rho_3(q)$. Thus $\rho_2(q) < \rho_3(q)$ and then :

$$ \rho_2(\text{remove}(q)) \le \rho_3(\text{remove}(q)).\square $$

Using these properties, it can be proved without difficulty that $\rho(=)$ is valid and that the axioms are preserved.

For instance, let us consider the axiom :

$$ \text{remove}(\text{append}(q,it)) = \text{if empty?}(q) \text{ then } \text{emptyq else append}(\text{remove}(q),it) $$

It must be proved that the representations of the left-hand side and of the right-hand side satisfy the relation $\rho(=)$. Let $\rho(q)=<a,i,j>$.

The left-hand side becomes :

$$ \rho(\text{remove}(\text{append}(q,it))) = \\ <\rho_1(\text{append}(q,it)), \rho_2(\text{append}(q,it))+1, \rho_3(\text{append}(q,it))) = \\ <\text{assign}(a,i,it), i+1, j+1> $$

The right-hand side becomes :

$$ \text{if } ?=(i,j) \text{ then } <\text{emptya},o,o> \text{ else } <\text{assign}(\rho_1(\text{remove}(q)),\rho_3(\text{remove}(q)),it),\rho_2(\text{remove}(q)),\rho_3(\text{remove}(q))+1)> $$

Then, we do a case analysis. If $?=(i,j)$ is true it comes :

$$ <\text{assign}(a,j,it),i+1,j+1> \rho(=) <\text{emptya},o,o> $$

and the axiom is conserved in this case.

If $?=(i,j)$ is false, then the right-hand side can be rewritten :

$$ <\text{assign}(a,j,it),i+1,j+1> $$

and is equal to the left-hand side.
It can be seen that, whatever the approach used, the specification of a
representation is simple and the correctness rules are elementary. The
simplicity of these correctness proofs leads to the thought that it may be
possible, from the representation of a subset of operations, to deduce the
complete representation systematically (and may even automatically). This
method would be more constructive than doing a long and tedious proof
"a posteriori". In [Gau 78] an example is given of a representation which
is completed starting only from the constructors representation and the
equality interpretation.

V. Conclusion

This paper is an attempt to point out the main ideas and results in the area of
algebraic abstract data type. One goal was to be as short as possible so that
the potential reader was not discouraged by a too long presentation. An important
field, the study of parametrized data types, such that "Queue of *anything*" or
"Set of *any-type-with-equality*" has been intentionally passed over. This essen-
tial point is discussed at length in several papers mentionned in the references :
[CHM 76, Go 77, TWW 78]. It is hoped that the reader has taken a fancy to
algebraic data types and will start an exhaustive study of the bibliography !

Acknowledgments :

I am indebted to John Guttag for his advices in the preparation of this course
and the licence he has given me to use material from some of his papers.
References

[BG 77] Burstall R.M, Goguen J.A, "Putting Theories Together to Make Specifications". Proceedings of the 5th International Joint Conference on Artificial Intelligence (1977) pp 1045-1058.

[Gau 78] Gaudel M.C. "Specifications Incomplètes mais Suffisantes de la Représentation des Types Abstraits" - Rapport Laboria n° 320, 1978.

[GDM 78] Gaudel M.C., Deschamp Ph. Mazaud M. "Semantics of Procedures as an Algebraic Abstract Data Type" - Rapport Laboria n° 334, 1978.

[GH 78] Guttag J.V., Horning J.J., "The Algebraic Specification of Abstract Data Types", Acta Informatica, 10,1 1978 - pp. 27-52.

[GHM 76] Guttag J.V., Horowitz E., Musser D.R, "Abstract Data Types and Software Validation", U.S.G. ISI Report 76-48 and C.A.C.M. Vol 21, n° 12, 1978 - pp. 1048-1064.

[Go 77] Goguen J.A., "Abstract Errors for Abstract Data Types", Formal Description of Programming Concepts, Neuhold Ed., 1977 - pp. 491-526.

[GP 79] Gaudel M.C., Pair C., "Construction de Compilateurs basés sur une Sémantique Formelle", Actes des Journées Francophones sur la Certification du Logiciel - Genève, 1979 - pp. 83-101.

[GTW 78] Goguen J.A., Thatcher J.W., Wagner E.G., "Abstract Data Types as Initial Algebras and the Correctness of Data Representations", Current Trends in Programming Methodology 4 - (Yeh R. Ed.) Prentice-Hall - 1978 - pp. 80-149.

[Gu 79] Guttag J.V., "Notes on Type Abstraction" (Version 2) to appear in IEEE Transactions on Software Engineering - 1979.

[Hoa 72] Hoare C.A.R., "Proofs of Correctness of Data Representations" Acta Informatica, Vol, n° 1, 1972 - pp. 271-281.
[KB 70] Knuth D.E., Bendix P.B., "Simple Word Problems in Universal Algebras", Computational Problems in Abstract Algebras, (J. Leech Ed.) Pergamon Press - 1970 - pp. 263-297.

[Mu 77] Musser D.R., "A Data Type Verification System Based on Rewrite Rules", Proceedings of the 6th Texas Conference on Computing Systems, Austin, Texas 1977.

[Sch 67] Schoenfield J.R., "Mathematical Logic" - Addison. Wesley 1967.

[SW 75] Spitzen J., Wegbreit B., "The Verification and Synthesis of Data Structures", Acta Informatica, Vol 4, 1975 - pp. 127-144.

[TWW 78] Thatcher J.W., Wagner E.G., Wright J.B., "Data Type Specification : Parametrization and the Power of Specification Techniques" - 10th Annual Symposium on Theory of Computing, San Diego, California - 1978 - pp. 119-132.

[WS 76] Wegbreit B., Spitzen J.M., "Proving Properties of Complex Data Structures", J.A.C.M., Vol 23, n° 2 - 1976 - pp. 389-396.