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