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

Abstract data types -- representation function

Representation function -- abstraction

$%a(%c)( %a(%f)) = %a(%f')$ $<=>$ $%c (%f) = %f'$

Sequences -- abstract domain

empty sequence -- $<< >>$
concatenation -- $< > \. < >$ $=$ $< >$

Specification


  type stack T {
   $s : seq   T$ ;
  axioms:
   ${ true } push(t:T) { s' = s \. < > }$ 
   ${ s \neq << >> } pop() { s = { s' } \. < > }$ 
  };

slide: The specification of a stack


  template    implementation  
  class as {
  int t;
  T a[MAX];
  public:
  as() { t = 0; }
  void push(T e) { 
         require(t0); return a[--t]; }
  
  invariant:
  	0 <= t && t < MAX;
  };

slide: The realization of a stack

Abstraction function

$%a(a,t) =$

Representation invariant

$I(a,t,s) == t = length(s) /\ t >= 0 /\ s = %a(a,t)$

slide: Abstraction function and representation invariant

Correspondence

$<< %a, %r, %x >>$

$%a$ abstraction -- maps $%s$ values to $%t$ values
$%r$ renaming -- maps subtype to supertype methods
$%x$ extension -- explains effects of extra methods

slide: The subtype correspondence mapping

Signature

$%s <= %t$

$dom( m_{%t} ) <= dom( m_{%s} )$
$ran( m_{%s} ) <= ran( m_{%t} )$

Behavior

$pre( m_{%t} )[ x_{%t} := %a( x_{%s} )] => pre( m_{ %s } )$
$post( m_{ %s } ) => post( m_{ %t } )[ x_{ %t } := %a( x_{ %s } ) ]$
$invariant( %s )$ $=>$ $invariant( %t )[ x_{ %t } := %a( x_{ %s } ) ]$

Extension -- diamond rule

$%x(x.m(a)) = %p_{m}$

$%f \apijl{ x.m(a) } %f' /\ %f \apijl{ %p_{m} } %Q$
$=>$ $%a( x_{ %f } ) = %a( x_{ %Q } )$

slide: Behavioral subtyping constraints

Behavioral subtypes

$stack <= bag$

bag -- put, get
stack -- push, pop, settop

Representation

bag -- $<< elems, bound >>$ \zline{multiset}
stack -- $<< items, limit >>$ \zline{sequence}

Behavior -- put/push


   $put(i):$ 
     $require   size( b.elems ) < b.bound$ 
     $promise   b' = << b. elems \uplus { i }, b.bound >>$ 
  
   $push(i):$ 
     $require   length( s.items ) < s.limit$ 
     $promise   s' = << s.items \. i, s.limit >>$

slide: Behavioral subtypes -- example

Correspondence

$stack -> bag$

%a(< >) =

<< mk_set( items ), limit >>

where


   $mk_set($ \%e ) = \0
   $mk_set( e \. s ) = mk_set(s) \uplus { e }$

$%r( push ) = put$ , $%r( pop ) = get$
$%x(s.settop(i))$ $=$ $s.pop(); s.push(i);$

slide: Behavioral subtypes -- correspondence

Proof obligations -- push/put

$size( %a(s). elems ) < %a(s).bound$
$=>$ $length( s.items ) < s.limit$
$s' = << s.items \. i, s.limit >>$
$=>$ $%a(s')$ $=$ $<< %a(s).elems \uplus { i }, %a(s).bound >>$

slide: Behavioral subtypes -- proof obligations

Æliens

2009

subsections:

Abstract data types -- representation function

Representation function -- abstraction

Sequences -- abstract domain

Specification

implementation

Abstraction function

Representation invariant

Correspondence

Signature

Behavior

Extension -- diamond rule

Behavioral subtypes

Representation

Behavior -- put/push

Correspondence

Proof obligations -- push/put