Abstract Data Type Examples

Because somebody was confused about ADTs and classes. ---

Depending on the programming language logic, ADTs can be defined in algebraic style (equations in which the terms are made by functional compositions and applications) or state based specifications (as in Hoare triples {Precondition} program {Postcondition}).

The prototypical ADT example is a Stack , which as an abstract data type, can be specified algebraically, as:

functions:

   Empty :  -> Stack.adt  /* (constructor, where Stack is the name of the module , ) */
   isempty : Stack.adt -> bool
   push : (Stack.adt x E) -> Stack.adt
   pop : Stack.adt -> Stack.adt  /* partially defined */
   top : Stack.adt  ->  E

axioms:

 isempty(Empty) = true
 isempty(push(s,e)) = false
 top(push(s,e)) = e
 pop(push(s,e)) = s

Or can be defined using Hoare triples :

 {true} s := Stack.Create; { isempty(s) }
 {true} push(s, e); { ! isempty(s) }
 {s = s0 } push(s,e); pop(s) { s=s0 }
 {true} push(s,e); e1 := top(s) { e=e1 }