<s5>Æliens</s5> -- slide(s)

Abstract data types

abstraction and types
algebraic specification
modules versus classes
types as constraints

Additional keywords and phrases: control abstractions, data abstractions, compiler support, description systems, behavioral specification, implementation specification

slide: Abstract data types

subsections:

Abstraction in programming languages
Foundational perspectives -- types as constraints
Objectives of typed OOP

Abstraction -- programming methodology

control abstractions -- structured programming
data abstraction -- information hiding

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). [DT88]

slide: Abstraction and programming languages

Abstract data types -- foundational perspective

unambiguous values in some semantic domain

Mathematical models -- types as constraints

algebra -- set oriented
second order lambda calculus -- polymorphic types
constructive mathematics -- formulas as types

slide: Mathematical models for types

Objectives of typed OOP -- system description

packaging in a coherent manner
flexible style of associating operations with objects
inheritance of description components -- reuse, understanding
separation of specification and implementation
explicit typing to guide binding decisions

slide: Object orientation and types

Bool">

Algebraic specification -- ADT

Bool


  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

slide: The ADT

Signature -- names and profiles

$%S$

$f : s_1 \* ... \* s_n -> s$

Functions -- for $T$

constants -- $c : -> T$
producers -- $g : s_1 \* ... \* s_n -> T$
observers -- $f : T -> s_i$

Type -- generators

$%S_T = P_T \cup O_T$ , $C_T \subset P_T$ , $P_T \cap O_T = \emptyset$

slide: Algebraic specification

Generators -- values of $T$

generator basis -- $G_T = { g \e P_T }$
generator universe -- $GU_T = { v_1, v_2, ... }$

Examples

$G_{Bool} = { t, f }$ , $GU_{Bool} = { t, f }$
$G_{Nat} = { 0, S }$ , $GU_{Nat} = { 0, S 0, SS 0, ... }$
$G_{Set_{A} } = { \emptyset, add }$ , $GU_{Set_{A} = { \emptyset, add(\emptyset,a), ... }$

slide: Generators -- basis and universe

Seq">

Sequences

$%e : seq T$
empty
$_ |> _ : seq T \* T -> seq T$
right append
$_ <| _ : T \* seq T -> seq T$
left append
$_ \. _ : seq T \* seq T -> seq T$
concatenation
$<< _ >> : T -> seq T$
lifting
$<< _,...,_ >> : T^{n} -> seq T$
multiple arguments

Generator basis -- preferably one-to-one

$G_{seq T } = { %e, |> }$ , $GU_{seq T } = { %e, %e |> a, %e |> b, ..., %e |> a |> b, ... }$
$G'_{seq T } = { %e, <| }$ , $GU'_{seq T } = { %e, a <| %e , b <| %e, ..., b <| a <| %e, ... }$
$G''_{seq T } = { %e, \. , << _ >> }$ , $GU''_{seq T } = { %e, < >, <$ >, ,..., %e \. %e, ..., %e \. <> , ... }

Infinite generator basis

$G'''_{seq T } = { %e, << _ >>, << _ , _ >>, ... }$ , $GU'''_{seq T } = { %e, < >, <$ >, ,..., <> , ... }

slide: The ADT

The equivalence relation -- congruence

$x = x$ \zline{reflexivity}

$x = y => y = x$ \zline{symmetry}

$x = y /\ y = z => x = z$ \zline{transitivity}

$x = y => f(...,x,...) = f(...,y,...)$

Equivalence classes -- representatives

abstract elements -- $GU_T /=$

slide: Equivalence

Nat">
Natural numbers

Nat

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

slide: The ADT

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

slide: Symbolic evaluation

Set">
Sets

Set

$G_{Set_{A} = { \emptyset, add }$

$GU_{Set_{A} }$ $=$ ${ 0, add(0,a), ..., add(add(0,a),a), ... }$

Axioms

[S1] $add(add(s,x),y) = add(add(s,y),x)$
commutativity
[S2] $add(add(s,x),x) = add(s,x)$
idempotence

slide: The ADT

Set">
Equivalence classes

$GU_{ Set _{A} }/=$

${ \emptyset }$

${ add(0,a), add(add(0,a),a), ... }$

$...$

${ add(add(0,a),b), add(add(0,b),a), ... }$

slide: Equivalence classes for

Mathematical model -- algebra

$%S$ -algebra -- $|A = ( { A_s }_{s \e S }, %S )$

interpretation -- $eval : T_{%S} -> |A$

adequacy -- $|A |= t_1 = t_2 <=> E |- t_1 = t_2$

slide: Interpretations and models

Bool and Nat">
Booleans

$|B = ( { tt, ff }, { \neg, / \/ } )$

$eval_{|B} : T_{Bool} -> |B = { or |-> \/, and |-> / not |-> \neg }$

Natural numbers

$|N = ( \nat , { ++ , + , \star } )$

$eval_{|N} : T_{Nat} -> |N = { S |-> ++ , mul |-> \star, plus |-> + }$

slide: Interpretations of

Initial algebra

$%S E$ -algebra -- $|M = ( T_{%S}/=, %S/=)$

Properties

no junk -- $\A a : T_{%S}/= \E t \dot eval_{|M}(t) = a$

no confusion -- $|M |= t_1 = t_2 <=> E |- t_1 = t_2$

slide: Initial models

Structure -- $ |B = ( {{ tt, ff }}, {{ \neg, /\, \/ }} )$

$|B$

$eval_{|B} : T_{%S_{Bool} -> |B = { or |-> \/, not |-> \neg }$

$eval_{|B} : T_{%S_{Nat} -> |B = { S |-> \neg, mul |-> / plus |-> xor }$

slide: Structure and interpretation

Stack">
Abstract Data Type -- applicative

Stack

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

slide: The ADT

Dynamic state changes -- objects

account

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

slide: The algebraic specification of an account

Multiple world semantics -- inference rules

$<< f(t_1,...,t_n),D >> -> << v, D >>$

attribute

$<< m(t_1,...,t_n),D >> -> << t_1, D' >>$

method

$<< t , D >> -> << t', D' >> => << e(...,t,...), D >> -> < >$

slide: The interpretation of change

ctr">
Example - a counter object

object ctr is
ctr
function n : ctr -> nat method incr : ctr -> ctr axioms n(new(C)) = 0 n(incr(C)) = n(C) + 1 end

slide: The object

Abstract evaluation

-[new]-> -[incr]-> -[incr]-> -[n]-> <2, { C[n:=2] }>

slide: An example of abstract evaluation

subsections:

Abstract interfaces

Representation and implementation

Adding new generators

Adding new observers

Modules -- a functional interface

ADT

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);

slide: Modules -- a functional interface

Objects -- a method interface

OOP

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; };

slide: Objects -- a method interface

Modules -- representation hiding

ADT

typedef int element; enum { NIL, CONS }; struct list { int tag; element e; list* next; };

Generators

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; }

slide: Data abstraction and modules

Modules -- observers

ADT

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); } }

slide: Modules -- observers

Method interface -- list

OOP

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; };

slide: Data abstraction and objects

Adding new generators -- representation

ADT

typedef int element; enum { NIL, CONS, INTERVAL }; struct list { int tag; element e; union { element z; list* next; }; };

Generator

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; }

slide: Modules and generators

Modifying the observers

ADT

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); } }

slide: Modifying the observers

Adding new generators

OOP

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; };

slide: Objects and generators

Adding new observers

ADT

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; }; }

slide: Modules and observers

Adding new observers

OOP

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 ); } };

slide: Objects and observers

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;

Types versus classes

types -- type checking predicates

classes -- templates for object creation

Type specification

syntactically -- signature
(under)

semantically -- behavior

(right)

pragmatically -- implementation
(over)

slide: Types and classes

Modifications

types -(predicate constraints) $->$ subtypes

classes -(template modification) $->$ subclasses

Varieties of (compatible) modifications

behaviorally -- algebraic, axiomatic

(type)

signature -- type checking

(signature)

name -- method search algorithm

(classes)

slide: Type modifications

Signature compatible modifications

behavior is approximated by signature

Semantics preserving extensions

horizontal -- Person = Citizen + { age : 0..120 }

vertical -- Retiree = Person + { age : 65..120 }

Principle of substitutability

an instance of a subtype can always be used in any context in which an instance of a supertype can be used

subsets are not subtypes
Retiree $\not<_{subtype}$ Person

Read-only substitutability

subset subtypes, isomorphically embedded subtypes

slide: The principle of substitutability

Name compatible modifications

operational semantics -- no extra compile/run-time checks

procedure search(name, module) if name = action then do action elsif inherited = nil then undefined else search(name, inherited)

slide: The inheritance search algorithm

Abstraction and types

1

abstraction -- control and data

abstract data types -- values in a semantic domain

types as constraints -- mathematical models

slide: Section 8.1: Abstraction and types

Algebraic specification

2

signature -- producers and observers

generator universe -- equivalence classes

initial model -- no junk, no confusion

objects -- multiple world semantics

slide: Section 8.2: Algebraic specification

Decomposition -- modules versus objects

3

data abstraction -- generators/observers matrix

modules -- operation-oriented

objects -- data-oriented

slide: Section 8.3: Decomposition -- modules versus objects

Types versus classes

4

types -- syntactically, semantically, pragmatically

compatible modifications -- type, signature, class

slide: Section 8.4: Types versus classes

Characterize the differences between control abstractions and data abstractions. Explain how these two kinds of abstractions may be embodied in programming language constructs.
How can you model the meaning of abstract data types in a mathematical way? Do you know any alternative ways?
Explain how types may affect object-oriented programming.
Explain how you may characterize an abstract data type by means of a matrix with generator columns and observer rows. What benefits does such an organization have?
How would you characterize the differences between the realization of abstract data types by modules and by objects? Discuss the trade-offs involved.
How would you characterize the distinction between types and classes? Mention three ways of specifying types. How are these kinds related to each other?
How would you characterize behavior compatible modifications? What alternatives can you think of?

slide: Questions

There is a vast amount of literature on the algebraic specification of abstract data types. You may consult, for example, [Dahl92].

Æliens

2009

Abstract data types

subsections:

Abstraction -- programming methodology

Abstract data types -- foundational perspective

Mathematical models -- types as constraints

Objectives of typed OOP -- system description

subsections:

Algebraic specification -- ADT

Signature -- names and profiles

Functions -- for $T$

Type -- generators

Generators -- values of $T$

Examples

Sequences

Generator basis -- preferably one-to-one

Infinite generator basis

The equivalence relation -- congruence

Equivalence classes -- representatives

Natural numbers

Sets

Axioms

commutativity

idempotence

Equivalence classes

Mathematical model -- algebra

Booleans

Natural numbers

Initial algebra

Properties

Structure -- $ |B = ( {{ tt, ff }}, {{ \neg, /\, \/ }} )$

Abstract Data Type -- applicative

Dynamic state changes -- objects

Multiple world semantics -- inference rules

Example - a counter object

ctr

Abstract evaluation

subsections:

Modules -- a functional interface

Objects -- a method interface

Modules -- representation hiding

Generators

nil

cons

Modules -- observers

head

tail

equal

Method interface -- list

nil

cons

Adding new generators -- representation

Generator

Modifying the observers

head

tail

Adding new generators

interval

Adding new observers

length

Adding new observers

length

listWL

Types versus classes

Type specification

Modifications

Varieties of (compatible) modifications

Signature compatible modifications

Semantics preserving extensions

Principle of substitutability

subsets are not subtypes

Read-only substitutability

Name compatible modifications

Abstraction and types

Algebraic specification

Decomposition -- modules versus objects

Types versus classes