ADT

ADT is the basic mathematical concept that defines the data type and stands for Abstract Data Type. Formally, ADT can be defined as a set of data values and the associated operations that are precisely specified, independent of any particular implementation.

Value Definition:
The Value definition defines the collection of values from the ADT and consists of two parts: A definition Clause (compulsory) and A Condition Clause (optional).

Operator Definition:
The operator definition consists of three parts: Header, Precondition and Post Condition.

An example of ADT.

abstract typedef <> STRING;

abstract length (s)
STRING s;
postcondition length = = len(s);

abstract STRING concat(s1,s2)
STRING s1,s2;
postcondition concat=s1+s2;

abstract STRING substr(s1, i, j)
STRING s1;
int i, j;
precondition 0 <= i < len(s);
0 <= j <= len(s1) – i;
postcondition substr = = sub(s1,i,j);

abstract pos(s1, s2)
STRING s1,s2;
postcondition

( ( pos = = -1) && (for( i=0; i <= lastpos; i++ ) (s2 <> sub(s1,i,,len(s2) ) ) ) )
| |
( ( pos >= 0) && ( pos <= lastpos) && ( s2 = = sub (str1, pos, len(s2) )

&& ( for( i=1; i sub(s1,i, len(s2) ) ) ) )