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


Scripts -- cooperation by enrollment

Multiparty interactions -- communication primitive

Joint action systems -- action-oriented

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