Epita:Algo:Course:Sup-Info: Abstract Data Types

Declarations

We define an abstract type with a signature and a set of axioms.

Signature

The signature of an abstract data type is composed of sorts (types) and operations. Using several sets of values ​​(integer, Binary Trees, and so on..), the types allow you to specify the name of the type(s) you want to define. For example:

stack, list, integer, graph, tree234

The operations allow you to name the specific property type(s) that you want to define. They are characterized by an identifier (name) and the formal declaration (profile) of their arguments as well as the type of their result. The declaration of the arguments is done using their type, thus:

insert: list x integer x element $\rightarrow$ list

declares the operation that inserts an element to the n^th place (defined in this case by a integer) of a list and returns a list.

In the algorithms, we use operations as functions, that is to say: the identifier, and in parentheses, its actual arguments corresponding to those defined formally. For example, if we want to use the insert operation using the variables l, i and e of respective type list, integer and element, we would have:

insert(l, i, e)

Operation identifiers can be created using all characters except the space character, parentheses, and the underscore character _ which are respectively used to separate identifiers, force operation priorities and place operation arguments. It's also possible to use glyphs. The following examples are valid:

operations

    factorial : integer $\rightarrow$ integer
        power : integer x integer $\rightarrow$ integer
 discriminant : integer x integer x integer $\rightarrow$ integer

or

           _! : integer $\rightarrow$ integer
          _^_ : integer x integer $\rightarrow$ integer
            Δ : integer x integer x integer $\rightarrow$ integer

Note: In the previous example, to avoid too many parentheses and/or when we refer to conventional operations like factorial or power, the name of the operation may specify the place of each argument using the underscore character _, as in _! and _^_. In this case, each parameter directly replaces the underscore character (in order of meeting). Similarly we see that we can use Δ instead of discriminant. These operations can be used like this:

x!		
x^y!	  (Laugh!)
(x^y)!   (Laugh again!)
Δ(x,y,z)

Note the use of parentheses to remove any ambiguity.

An operation whose profile does not require any argument is a constant, for example:

   0 : $\rightarrow$ integer
False: $\rightarrow$ boolean
  pi : $\rightarrow$ real

At last a complete example of signature, the Boolean type:

types

   boolean

operations

    true : $\rightarrow$ booléean
   false : $\rightarrow$ boolean
     not : boolean $\rightarrow$ boolean
     and : boolean x boolean $\rightarrow$ boolean
      or : boolean x boolean $\rightarrow$ boolean

Hierarchy of abstract types

We have the ability to define an abstract type reusing those previously defined. Indeed, if someone has got operations manipulating integers, it's better not to have to redefine the type integer. Many basic types are considered as predefined. Among them we find the types integer, real, boolean, and so on...

For example, to define a type vector, we are going to reuse types integer and element. Data represented by the type element can be anything: numbers, clothes, car wheels (why not car wheels? Aren't car wheels nice ?) and the type integer, as for it, will represent... Well, integers (Incredible!). A hierarchy is created between types: Those we are trying to define and those that are already created.

types

   vector

uses

   integer, element

operations

       modify : vector x integer x element $\rightarrow$ vector
          nth : vector x integer $\rightarrow$ element
   lowerlimit : vector $\rightarrow$ integer
   upperlimit : vector $\rightarrow$ integer

In this case, the signature of type vector is the union of the signature of types integer and element to which are added new operations that characterize the type vector. Therefore, we may use previously defined operations on used types, such as the addition of integers. For instance, the operation nth (to cite one) will use for the 2^nd argument the sum of two integers:

nth(v,i+2)		

This hierarchy allows us to say that a type is:

• defined if it's new ("under design", specified in types)
• Predefined if exists ("already designed" and specified in uses).

Similarly, we say that an operation is:

• an internal operation if it returns a result of type defined,
• An observer, if it has at least one argument of type defined and returns a result of type predefined.

We could define it otherwise and say that in fact the internal operations are these that change the state of the data itself, while observers, as their name suggests, merely observe and return a value located where they are asked to watch.

In the previous example, vector is a defined type, integer and element are predefined types, which make modify an internal operation and nth, lowerlimit and upperlimit observers.

abstract type properties

The idea is to give meaning to signature identifiers. That is to say that when we talk about a kind of data, all its possibilities and limitations will immediately be known (If I say stack, I know I can't make coffee :)). In this case if we want to detach them from all implementation contingencies, we have to define operation properties as axioms. This is more commonly called an axiomatic definition or an algebraic definition.

The problem is to define what does an internal operation. To find it out, we just have to apply its own observers. Values ​​obtained by these applications allow us to understand how the internal operation works.

For example the application of the observer nth to the internal operation modify, gives the following two axioms:

  lowerlimit(v) ≤ i ≤ upperlimit(v) $\Rightarrow$ nth(modify(v,i,e),i)=e
  lowerlimit(v) ≤ i ≤ upperlimit(v) & lowerlimit(v) ≤ j ≤ upperlimit(v) & i≠j 
     $\Rightarrow$ nth(modify(v,i,e),j)=nth(v,j)

The first axiom says that when we call modify with a vector v, an integer i and an element e, the element e is placed in the i^th box of the vector v. This is shown by the observer nth that applied with the same integer i to the new vector (the one created by modify) is equal to e.

The second axiom, always using the observer nth, specifies that only the i^th box of the vector v is amended by element e and that all other boxes referenced by the integer j ≠ i have retained the element contained in the vector v (before change).

Note: The definition of an algebraic abstract type is composed of a signature and a system of axioms that characterize it.

After the set of axioms is established, we must verify two things:

• The lack of contradictory axioms called consistency. The opposite is when applying the same operation to identical arguments it gives different values.

• Having written enough axioms called completeness, which corresponds to being able to deduce a value for any application of an observer to an internal operation.

In general, an object is complete if nothing needs to be added to it. This notion is made more specific in various fields. In algorithms, the notion of completeness refers to the ability of the algorithm to find a solution if one exists, and if not, to report that no solution is possible.'

In math, a theory T and consequently a system of axioms that defines it is complete if it is consistent and if for any formula "P" without variable, you are able to show either P or not P.

But this définition is too strong for Algebraic abstract types. It implies that each quality between two expressions must be true or not. But coders need more freedom than this allows.

For example: In a vector v, we are modifying, in this order, the 5th box value in a and the 10th box value in b. If we change the order (b at first and a at second), it is equal. But what about using a linked list implementation of (index,element) couples where modify add just a couple at list head ? The most important is that when we apply nth to these two vectors, we obtain the same result. The fact that they are equals is not essential.

So we talk about sufficient completeness. That means: Axioms allow us to deduce a value of predefined type by application of an observer to an defined type object. As we get these objects by internal operation applications, we have to write axioms that allow us to deduce a value of predefined type by application of observers to internal operations.

Nevertheless there are operations that are not described everywhere (nobody's perfect). They are called partial. In this case, before writing axioms using these operations, you must specify their domain of definition. This is done in the preconditions part.

For instance : The top of a stack is not defined on an empty stack

Then we rephrase the rule : axioms allow us to deduce a value by application of observers to internal operations on observer definition domain.

Finally, take again the example of the vector and give the completeness definition:

types

   vector

uses

   integer, boolean, element

operations

         vect : integer x integer $\rightarrow$ vector
       modify : vector x integer x element $\rightarrow$ vector
          nth : vector x integer $\rightarrow$ element
       isinit : vector x integer $\rightarrow$ boolean
   lowerlimit : Vector $\rightarrow$ integer
   upperlimit : vector $\rightarrow$ integer

preconditions

   nth(v,i) is defined if-and-only-if lowerlimit(v) ≤ i ≤ upperlimit(v) & isinit(v,i) = true

axioms

   lowerlimit(v) ≤ i ≤ upperlimit(v) $\Rightarrow$ nth(modify(v,i,e),i)=e
   lowerlimit(v) ≤ i ≤ upperlimit(v) & lowerlimit(v) ≤ j ≤ upperlimit(v) & i≠j 
      $\Rightarrow$ nth(modify(v,i,e),j) = nth(v,j)

   isinit(vect(i,j),k) = false
   lowerlimit(v) ≤ i ≤ upperlimit(v) $\Rightarrow$ isinit(modify(v,i,e),i) = true
   lowerlimit(v) ≤ i ≤ upperlimit(v) & lowerlimit(v) ≤ j ≤ upperlimit(v) & i≠j 
      $\Rightarrow$ isinit(modify(v,i,e),j) = isinit(v,j)

   lowerlimit(vect(i,j)) = i
   lowerlimit(modify(v,i,e)) = lowerlimit(v)

   upperlimit(vect(i,j)) = j
   upperlimit(modify(v,i,e)) = upperlimit(v)

with
    vector v
   integer i,j,k
   element e

Spontaneous generation doesn't exist in Algorithms. So we add the operation vect which creates a vector from its limits (lower and upper represented by two integers). On the other hand, the operation nth is partial, it's indeed not defined for a box to which we wouldn't have previously assigned an element (using modify). So we had to add an auxiliary operation isinit whose the only purpose is to enable writing a precondition for nth, that is to say : define the domain of definition of nth.

To conclude with this example, the design and understanding of the algebraic abstract vector type definition is consistent and complete for the following reasons:

• There is no axiom in contradiction with one another.
• Any vector is the result of an operation vect and a series of operations modify, effects observed by isinit, lowerlimit and upperlimit in all cases and by nth when the precondition is satisfied.

---

(Christophe "krisboul" Boullay)