General ADT features

In this subsection a general introduction to the ADT concept is given.
Subsequent sections treat typical ADT features of SDL-88.

Basic features

With a specification language it should be possible to specify a system on an appropriate level of abstraction, and as implementation independent as possible. Usually, abstraction allows to point out important features of an object while irrelevant details are omitted. This also holds for data abstraction.

The concept of ADT is suitable in cases where the functional properties of a data object should be described. An ADT defines the result of the application of a function to a certain data object, but it does not tell how these results should be achieved. The latter is up to an implementation of the data object.

In the most simple case, an ADT is a set of values, hereafter called sort, together with a number of operators on this set. For example the set of natural numbers, together with the addition and multiplication operator, form an ADT. In mathematical notation, an ADT can be written down as a n-tuple, where the first component is a set and the second to n-th components are operators. Therefore we could call (N,+,*) an abstract data type.

In general an ADT can consist of more than one sort, and the operators may have arguments of different sorts, but the results of the operators are always in one of the sorts. In the following we will develop an example in which the ADT has the sorts natural numbers and boolean. and various operators on these. As a summary, one can say that

ADT = sorts + operators

The signature

For the definition of an ADT, we must first define the names of the sorts and operators, and the domains and ranges of the operators. The notation used in the following examples resembles the notation usually used in literature, e.g. [8].

ADT example

SORTS bool, nat
OPNS true    :                  ->bool
        false     :                  ->bool
        not       : bool          -> bool
        0         :                   ->nat
        1         :                   ->nat
        plus     : nat, nat   ->nat
        isZero  : nat            ->bool

In the example above, two sort names and 7 operator names are defined. Together with the names of the operators, the domains and ranges are defined. Please note that some of the operators do not have arguments, like true false, 0 and 1. Such operators are called literals.

The names of the sorts and operators, together with the definition of domains and ranges, are called signature of the ADT.

Terms

The literals define part of the elements of a sort. In general, a sort may have many more elements.

The entirety of the elements of a sort can be generated by repeated application of the operators to the elements of the sort. A combination of applications of operators is called a term. A term is always of a certain sort, i.e. the range of the outermost one.

Examples of terms of the boolean sort are:

true,
false,
not(true),
not(false)
not(not(true) ), ...

Terms represent elements of a sort. A term which represents an element of a sort s, is-called s-term. The terms in the example above are therefore called bool-terms.

Every bool-term of the example above can be interpreted as an element of the bool sort. This example already shows, though, that it is not desirable that there is a one to one relationship between terms and elements of a sort. In general, the set of terms will be much larger than the set of elements of a sort.

Given the signature of an ADT, we can successively generate the set of terms. At the beginning we have the terms

{1,0,true,false}.

In the next successive step, for every operator from the entire set of operators of the ADT, terms are generated by applying the operators to the set of existing terms. After this step, we have the set of terms

{1, 0, true, false,
plus(1,1), plus(1,0), plus(0,1), plus(0,0),
not(true), not(false),
isZero(1). isZero(0)}

Now we can apply the successive step again to generate more terms. Please note that in this example in the set of generated terms there are terms of two different sorts

The successive generation of terms results in an infinite number of terms.

Equations

Equations between terms specify which terms represent the same element of a given sort. For example, the equation

not(true) = false

specifies that the term not(true) and the term false represent the same value of the sort bool.

With a set of equations, the set of terms can be divided into equivalence classes. Every equivalence class then represents an element of the sort. In our example, the set of bool-terms is divided into equivalence classes by the two equations

not(true) = false,
not(false) = true.

The respective equivalence classes are

{true, not(false), not(not(true)),...},
{false, not(true),not(not(false)),...}.

The equations can also be interpreted in another way. Equations specify properties of operators. The properties of the not operator, for example, are that it satisfies the equations above.

The equations can be defined in any order. Our ADT example can now be extended in the following ways:

ADT example

SORTS bool, nat
OPNS true : ->bool
        false : ->bool
        not : bool -> bool
        0 : ->nat
        1 : ->nat
        plus : nat, nat ->nat
        isZero : nat ->bool
EQNS not(true) = false
        not(false) = true
        …

Sometimes it is not possible to specify all desired properties of an operator with a finite set of equations. With variables and the FORALL construct, the equations can be "parameterised". Examples can be found in the following subsection.

Construction of a sort by the use of equations

The reduction of the set of terms, representing different elements of a sort, shall now be demonstrated with the plus operator. In the following, the properties, i.e. the equations, for the plus operator are introduced stepwise. plus generates the following nat-terms

0                                                 <- terms without plus
1
plus (n , 0)                                <- terms with one plus
plus (C, 1)
plus (1, 0)
plus (1 , 1 )
plus (plus (0, 0), 0)                 <- terms with two plus
plus (plus (0, 0) ,1)
plus (plus (0, 1), 0)
plus (plus (0, 1), 1 )
plus (plus (1, 0), 0)
plus (plus (1, 0), 1 )
plus (plus (1, 1), 0)
plus (plus (1, 1), 1)
plus (0, plus (0, 0) )
plus (0, plus (0, 1) )
plus (0, plus (1 0))
plus (0, plus(1,1))
plus (1 ,plus (0, 0) )
plus (1 plus (0, 1) )
plus (1, plus (l, 0))
plus (1, plus (1, 1))
…                                                 <- terms with three plus
…

The symmetry property of the addition

The amount of terms representing different elements of the nat-sort can be reduced by introducing the symmetry property of the addition. For any terms x and y, the terms plus (x, y) and plus (y, x) shall be identical. We specify this property by a parameterised equation:

FOR ALL x, y: nat
        plus (x, y) = plus (y. x)

With this equation the set of terms representing different elements of the nat-sort is reduced to the following

0                                            <- terms without plus
1
plus (0, 0)                            <- terms with one plus
plus (0, 1)
plus (l, 1)
plus (plus (0,0), 0)             <- terms with two plus
plus (plus (0, 0), 1 )
plus (plus (0, 1), 0)
plus (plus (0, 1), 1)
plus (plus (1, 1), 0)
plus (plus (1, 1), 1)
…                                         <- terms with three plus
…                                         …

Addition of zero

The next property we want to specify is that addition of zero has no effect This can be specified by the following equation:

FORALL x: nat
        plus (x, 0) = x

With this equation the set of terms representing different elements of the nat-sort is reduced to the following

0                                                                     <- terms without plus
1
plus (1, 1)                                                      <- terms with one plus
plus (plus (1, 1), 1)                                       <- terms with two plus
plus (plus (plus (1, 1), 1), 1)                        <- terms with three plus
plus (plus (plus (plus (1, 1), 1), 1), 1)        <- terms with four plus

We can now try to relate the remaining terms to the natural numbers:

0                                                     = zero
1                                                     = one
plus (1, 1)                                      = two
plus (plus (1, 1), 1)                       = three
plus (plus (plus (1, 1), 1), 1)       = four
plus (plus (1, 1), plus (1, 1)        = four
…                                                    …

The "addition" property of the addition

Something is still unsatisfying: the terms

plus (plus (1, 1), plus (1, 1)),
plus (plus (plus (1, 1), 1), 1)

specify the same element. Also, we have not said anything about the most important property of the plus operator, namely the property that it really adds two numbers and gives the correct result, e.g. 3 + 2 = 5, or in the terminology from above

plus (plus (plus (1, 1), 1), plus (1, 1) ) =
plus (plus (plus (plus (1, 1), 1), 1), 1)

Both problems can be solved by one additional equation:

FORALL x, y: nat
plus (x, plus (y,1)) = plus (plus (x, y),1)

With this equation it can be shown by induction on the number of plus in a term, that any term can be written in one of the forms

0,
1,
plus (plus (.. (plus (1, 1), …, 1), 1)

and that the addition property manly holds.

A complete definition of the ADT example, including the equations for the operator isZero, can now be given as follows:

ADT example

SORTS bool, nat
OPNS true : ->bool
        false : ->bool
        not : bool -> bool
        0 : ->nat
        1 : ->nat
        plus : nat, nat ->nat
        isZero : nat ->bool
EQNS not(true) = false
        not(false) = true
        FORALL x, y: nat
                plus (x , y ) = plus (y , x)
                plus (x, 0) = x
                plus (x, plus(y, 1)) = plus (plus (x, y),1)
                isZero (0) = true
                isZero (plus (x, 1)) = false

The SDL data type concept

An SDL system description is constructed in a hierarchical manner. and the structure can be represented as a tree. such as the one in figure 4. At any place in the tree there may be descriptions of sorts, operators and equations.

Figure 4 (from Basic system structure)

A sort is specified in SDL, together with operators and equations, in so called partial type definitions.

At any point in a system description tree, there is only one abstract data type. It is defined by the sorts, operators and equations introduced by the partial type descriptions from the root of the tree to the point in question.

Consider process P11 in figure 4: the ADT at this point is defined by the partial type definitions in P11, B1 and S.

If (for example) in S the partial type definition has:
    sorts: sor1, sor2,
    operators: op1, op2, op3, and
    equations: eq1, eq2

and in B1 the partial type definition has:
    sorts: sorA, sorB, sorC
    no operators, and
    equation: eqA

and in P11
    no sorts are defined, but the there is are definitions of
    operators opA, opB, and
    equation: eqB

then implicitly in P11 the  complete ADT with
    sorts: sor1, sor2, sorA, sorB, sorC,
    operators: op1, op2, op3, opA, opB, and
    equations: eq1, eq2, eqA, eqB

is defined and can, for example, be used to declare data. 

An ADT thus only exists implicitly in SDL, and does not have a name. Partial types which are not defined in the direct hierarchy of a certain process (or block) are not relevant for this process (or block, respectively). Thus in the example of figure 4 it is completely irrelevant for P11 which partial types are defined in B2 or P21. Certain rules have to be obeyed when specifying partial data types hierarchically. For these the reader is referred to [1].

Contact the webmaster with questions or comments about this web site.
Copyright © 1997-August, 2007 SDL Forum Society