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

Behavioral refinement

types as behavior
verification
abstraction and representation
behavioral compositions

Additional keywords and phrases: behavioral subtypes, state transformers, correctness formulae, assertion logic, transition systems, invariants, formal specification

slide: Behavioral refinement

Subtype requirements -- signature and behavior

preservation of behavioral properties

Safety properties -- nothing bad

invariant properties -- true of all states
history properties -- true of all execution sequences

slide: Subtyping and behavior

Example -- $IntSet \not<= FatSet$

FatSet -- insert, select, size
IntSet -- insert, delete, select, size

History property -- not satisfied by $IntSet$

$\A s : FatSet. \A %f, %q : State. %f < %q /\ s \e dom (%q).$
\hspace{2cm} $\A x : Int. x \e s_{%f} => x \e s_{%q}$

slide: History properties -- example

Types as behavior -- constraints

$x : 9..11$ $<=>$ $x : Int /\ 9 <= x <= 11$

Behavioral constraints -- signature versus assertions

$f(x:9..11) : 3..5 { ... }$


    int f(int x) {
       require( 9 <= x  && x <= 11 );
       ...
       promise( 3 <= result && result <= 5);
       return result;
       }

slide: Types and behavioral constraints

Substitutions


  \%f [x:=v](y)  ==
         v             if  $x = y$ 
         \%f (y)        otherwise

slide: Substitution

Program state -- $%f$

$%f \e %S : Var -> Value$

State transformations -- operations $a_1,a_2,...,a_n$

$%f_{0} -{a_1}-> %f_{1} ... -{a_n}-> %f_n$

Correctness formulae -- Hoare logic

${ P } S { Q }$

Verification

$%f_i -{a}-> %f_j /\ %f_i |= P => %f_j |= Q$

slide: The verification of state transformations

Axioms

assignment -- ${ Q [x:=e] } x = e { Q }$
composition -- ${ P } S1 { R } /\ { R } S2 { Q } => { P } S1;S2 { Q }$
conditional -- ${ P /\ b } S { Q } => { P } if (b) S { Q }$
iteration -- ${ I /\ b } S { I } => { I } while (b) S { I /\ \neg b }$

Consequence rules

$P -> R /\ { R } S { Q } => { P } S { Q }$
$R -> Q /\ { P } S { R } => { P } S { Q }$

Procedural abstraction

$m(x) |-> S(x) /\ { P } S(e) { Q } => { P } m(e) { Q }$

slide: The correctness calculus

Expressions

syntax

$e ::= v | x.v$

Elementary statements

$s ::= v = e | x = new %t | x.m(e)$

Compound statement

$S ::= %e | s | S1;S2 | \! if (b) S | while (b) S$

slide: The syntax of a simple OO language

Assignment

rules

$<< v = e, %f^{%a} >> -> << %e, %f [ %a.v := e_{%f} ] >>$

Object creation

\ffrac{ $<< S_{%t}, %f^{%a} >> \apijl{%l} << %e, %f' >>$ }{ $<< x \! = \! new %t, %f >> \! \apijl{ %a \. %l } \! << %e , %f'[ x \! := %a \! ]>>$ }

Method call

\ffrac{ $<< S_m(e), %f^{%a} >> \apijl{%l} << %e, %f' >>$ }{ $<< x.m(e), %f >> \apijl{ m_{%a} \. %l } << %e, %f' >>$ }

slide: Transition system -- rules

Composition

compound

\ffrac{ $<< S_1, %f >> \apijl{ %l_1 } << %e, %f' >>$ \ifsli{\hspace{-0.5cm}}{\hspace{1cm}} $<< S_2, %f' >> \apijl{ %l_2 } << %e, %f'' >>$ }{ $<< S_1;S_2, %f >> \apijl{ %l_1 \. %l_2 } << %e, %f'' >>$ }

Conditional

$<< \! if (b) S, %f>> -> << %e, %f>>$ if $%f(b) == false$
\ffrac{ $<< S, %f >> \apijl{%l} << %e, %f' >>$ }{ $<< \! if (b) S, %f >> \apijl{%l} << %e, %f' >>$ } if \ifsli{ $%f(b)$ }{ $%f(b) == true$ }

Iteration

$<< while \; (b) S, %f>> -> << %e, %f>>$ if $%f(b) == false$
\ffrac{ $<< S, %f >> \apijl{%l} << %e, %f' >>$ }{ $<< while (b) S, %f >> \apijl{%l} << while (b) S, %f' >>$ } \ifsli{}{ if $%f(b) == true$ }

slide: Transition system -- compound statement

Program

$x = new ctr; x.inc(); v = x.n$

Transitions

$<< x = new ctr, %f_1 >> \apijl{ctr_1} << %e, %f_1[ x := ctr_1 ]>>$

$[1]$

$<< n = n + 1, %f_2^{%a} >> -> <<%e, %f_2[%a.n = %a.n + 1]>>$

$[2]$

$<< x.inc(), %f_2 >>$ $\apijl{inc_{%a}$ $<< %e, %f_2[%f_2(x).n := %f_2(x).n ]>>$

$[2']$

$<< v = x.n, %f_3>> -> << %e, %f_3[v := %f_3(x).n] >>$

$[3]$

Trace

$%f \apijl{%l} %f'$ with $%f = %f_1$ , $%f' = %f_3$ and $%l = ctr_1 \. inc_{ %a }$

slide: Transitions -- example

subsections:

Abstraction and representation
Correspondence

Abstract data types -- representation function

Representation function -- abstraction

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

slide: Abstraction and representation

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

Problem -- dynamic aliasing


  class A {
  public:
  A() { forward = 0; }
  attach(B* b) { forward = b; b->attach(this); }
  bool invariant() {
     return !forward || forward->backward == this;
     }
  private:
  B* forward;
  };
  
  class B {
  public:
  B() { backward = 0; }
  attach(A* a) { backward = a; }
  bool invariant() {
     return !backward || backward->forward == this;
     }
  private:
  A* backward;
  };

slide: Establishing global invariants


  A a1, a2; B b;
  a1.attach(b);
  a2.attach(b); // violates invariant a1

Contracts -- behavioral compositions

interaction

specification, refinement, conformance declarations

Scripts -- cooperation by enrollment

roles, initialization/termination protocols, critical role set

Multiparty interactions -- communication primitive

frozen state, fault-tolerance, weakening synchrony

Joint action systems -- action-oriented

state charts, refinement, superposition

slide: Specifying interactions

Joint action systems


  action  $service()$  by client c; server s is
  when c.requesting && s.free do
  	<body>

slide: Specifying actions -- example


  contract model-view< V > {    MV(C)  
  subject : model supports [
   state : V;
   value( val : V )  $|->$  [state = val]; notify(); 
   notify()  $|->$   $\forall v \e$ views  $\bl$  v.update(); 
   attach( v : view )  $|->$  v  $\e$  views;
   detach( v : view )  $|->$  v  $\not\e$  views;
   ]
  views : set where view supports [
   update()  $|->$  [view reflects state];
   subject( m : model )  $|->$  subject = m;
   ]
  invariant:
    $\forall$  v  $\e$  views  $\bl$  [v reflects subject.state]
  instantiation:
    $\forall$  v  $\e$  views  $\bl$  subject.attach(v) & v.subject(subject);
   subject.notify();
  }

slide: The Model-View contract

Æliens

2009

Behavioral refinement

Subtype requirements -- signature and behavior

Safety properties -- nothing bad

Example -- $IntSet \not<= FatSet$

History property -- not satisfied by $IntSet$

Types as behavior -- constraints

Behavioral constraints -- signature versus assertions

subsections:

Substitutions

Program state -- $%f$

State transformations -- operations $a_1,a_2,...,a_n$

Correctness formulae -- Hoare logic

Verification

Axioms

Consequence rules

Procedural abstraction

Expressions

Elementary statements

Compound statement

Assignment

Object creation

Method call

Composition

Conditional

Iteration

Program

Transitions

Trace

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

Problem -- dynamic aliasing

Contracts -- behavioral compositions

Scripts -- cooperation by enrollment

Multiparty interactions -- communication primitive

Joint action systems -- action-oriented

Joint action systems

MV(C)