The history of programming languages may be characterized as the genesis of increasingly powerful abstractions to aid the development of reliable programs.
Additional keywords and phrases:
control abstractions, data abstractions,
compiler support,
description systems,
behavioral specification,
implementation specification
The kind of abstraction provided by ADTs can be supported
by any language with a procedure call mechanism
(given that appropriate protocols are developed
and observed by the programmer).
adt bool is functions true : bool false : bool and, or : bool * bool -> bool not : bool -> bool axioms [B1] and(true,x) = x [B2] and(false,x) = false [B3] not(true) = false [B4] not(false) = true [B5] or(x,y) = not(and(not(x),not(y))) end
empty
right append
left append
concatenation
lifting
multiple arguments
functions 0 : Nat S : Nat -> Nat mul : Nat * Nat -> Nat plus : Nat * Nat -> Nat axioms [1] plus(x,0) = x [2] plus(x,Sy) = S(plus(x,y)) [3] mul(x,0) = 0 [4] mul(x,Sy) = plus(mul(x,y),x) end
mul(plus(S 0,S 0),S 0) -[2]-> mul(S(plus(S 0,0)), S 0) -[1]-> mul(SS 0,S 0) -[4]-> plus(mul(SS0,0),SS0) -[3]-> plus(0,SS0) -[2*]-> SS0
[S1] $add(add(s,x),y) = add(add(s,y),x)$commutativity
[S2] $add(add(s,x),x) = add(s,x)$idempotence
$ |N |= eval_{|N}(t_1) =_{|N} eval_{|N}(t_2) <=> E_{Nat} |- t_1 = t_2 $
$f_{|M}([t_1],...,[t_n]) = [ f(t_1,...,t_n) ] $
functions new : stack; push : element * stack -> stack; empty : stack -> boolean; pop : stack -> stack; top : stack -> element; axioms empty( new ) = true empty( push(x,s) ) = false top( push(x,s) ) = x pop( push(x,s) ) = s preconditions pre: pop( s : stack ) = not empty(s) pre: top( s : stack ) = not empty(s) end
object account is functions bal : account -> money methods credit : account * money -> account debit : account * money -> account error overdraw : money -> money axioms bal(new(A)) = 0 bal(credit(A,M)) = bal(A) + M bal(debit(A,M)) = bal(A) - M if bal(A) >= M error-axioms bal(debit(A,M)) = overdraw(M) if bal(A) < M end
$fn(method(Object,Args))\; =\; expr$
$bal(credit(accountJohn,200))\; =\; bal(accountJohn)\; +\; 200$
attribute
method
object ctr is
ctr
function n : ctr -> nat method incr : ctr -> ctr axioms n(new(C)) = 0 n(incr(C)) = n(C) + 1 end
-[new]-> -[incr]-> -[incr]-> -[n]-> <2, { C[n:=2] }>
nil | cons(h,t) | |
---|---|---|
empty(l) | true | false |
head(l) | error | h |
tail(l) | error | t |
typedef int element; struct list; extern list* nil(); extern list* cons(element e, list* l); extern element head(list* l); extern list* tail(list* l); extern bool equal(list* l, list* m);
template< class E > class list { public: list() { } virtual ~list() { } virtual bool empty() = 0; virtual E head() = 0; virtual list* tail() = 0; virtual bool operator==(list * m) = 0; };
typedef int element; enum { NIL, CONS }; struct list { int tag; element e; list* next; };
list* nil() {
nil
list* l = new list; l->tag = NIL; return l; } list* cons( element e, list* l) {
cons
list* x = new list; x->tag = CONS; x->e = e; x->next = l; return x; }
int empty(list* lst) { return !lst || lst->tag == NIL; } element head(list* l) {
head
require( ! empty(l) ); return l->e; } list* tail(list* l) {
tail
require( ! empty(l) ); return l->next; } bool equal(list* l, list* m) {
equal
switch( l->tag) { case NIL: return empty(m); case CONS: return !empty(m) && head(l) == head(m) && tail(l) == tail(m); } }
list* r = cons(1,cons(2,nil())); while (!empty(r)) { cout << head(r) << endl; r = tail(r); }
template< class E > class nil : public list< E > {
nil
public: nil() {} bool empty() { return 1; } E head() { require( false ); return E(); } list< E >* tail() { require( 0 ); return 0; } bool operator==(list* m) { return m->empty(); } }; template< class E > class cons : public list< E > {
cons
public: cons(E e, list* l) : _e(e), next(l) {} ~cons() { delete next; } bool empty() { return 0; } E head() { return _e; } list * tail() { return next; } bool operator==(list * m); protected: E _e; list * next; };
list<int>* r = new cons<int>(1, new cons<int>(2, new nil<int>)); while (! r->empty()) { cout << r->head() << endl; r = r->tail(); } delete r;
typedef int element; enum { NIL, CONS, INTERVAL }; struct list { int tag; element e; union { element z; list* next; }; };
list* interval( element x, element y ) { list* l = new list; if ( x <= y ) { l->tag = INTERVAL; l->e = x; l->z = y; } else l->tag = NIL; return l; }
element head(list* l) {
head
require( ! empty(l) ); return l->e; // for both CONS and INTERVAL } list* tail(list* l) {
tail
require( ! empty(l) ); switch( l->tag ) { case CONS: return l->next; case INTERVAL: return interval((l->e)+1,l->z); } }
class interval : public list<int> {
interval
public: interval(int x, int y) : _x(x), _y(y) { require( x <= y ); } bool empty() { return 0; } int head() { return _x; } list< int >* tail() { return (_x+1 <= _y)? new interval(_x+1,_y): new nil<int>; } bool operator==(list@lt;int>* m) { return !m->empty() && _x == m->head() && tail() == m->tail(); } protected: int _x; int _y; };
int length( list* l ) {
length
switch( l->tag ) { case NIL: return 0; case CONS: return 1 + length(l->next); case INTERVAL: return l->z - l->e + 1; }; }
template< class E > int length(list< E >* l) {
length
return l->empty() ? 0 : 1 + length( l->tail() ); } template< class E > class listWL : public list<E> {
listWL
public: int length() { return ::length( this ); } };
list<int>* r = new cons<int>(1,new cons<int>(2,new interval(3,7))); while (! r->empty()) { cout << ((listWL< int >*)r)->length() << endl; r = r->tail(); } delete r;
(under)
(right)
(over)
(type)
(signature)
(classes)
subsets are not subtypes
Retiree $\backslash not<\_\{subtype\}$ Person
set_age : Person * Integer -> Void
Person* p = r;r refers to some Retiree
p->set_age(40);
procedure search(name, module) if name = action then do action elsif inherited = nil then undefined else search(name, inherited)
There is a vast amount of literature on the algebraic
specification of abstract data types.
You may consult, for example,
draft version 0.1 (15/7/2001)