subsections:

Object-oriented modeling

slide: Relations between objects

State and operations

Z


  • state == [ decls | constraints ]
  • op == [ %D state; decls | constraints ]

Change and invariance

  • %D state == state /\ state'
  • %X state == state = state'

Verification
  • state /\ pre( op ) => op
slide: Model-based specification
Counter in Z">

State

Counter 


  
  \begin{schema}{Counter}
  n : \nat
  \where
  n \geq 0
  \end{schema}

Operations

 
  
  \begin{schema}{Incr}
  \Delta Counter
  \where
  \mbox{  n' = n + 1  }
  \end{schema}
  
  \begin{schema}{Decr}
  \Delta Counter
  \where
  n > 0 \\
  \mbox{  n' = n - 1  }
  \end{schema}
slide: The specification of a
Counter">

Counter

Z 


   Counter \defs [ n : \nat | n \geq 0 ] 
   Counter::Incr \defs [ \%D Counter, v? : \nat | n' = n + v? ]
   Counter::Decr \defs [ \%D Counter | n > 0;  n' = n - 1 ]
   Counter::Value \defs [ \%X Counter; v! : \nat | v! = n ]

Bounded counter

 

   Bounded::Counter \defs [ Counter | n \leq Max ]
   Bounded::Incr \defs [ Counter::Incr | n < Max ]
slide: An alternative specification of the

State

Library (1) 


  
  \begin{schema}{Library}
  books : \power Book \\
  borrowed : Book \pfun Person
  \where
  \dom borrowed \subseteq books
  \end{schema}
slide: The specification of a library

Operations

Library (2) 


  
  \begin{schema}{Borrow}
  \Delta Library; b? : Book; p? : Person
  \where
  b? \not\in \dom borrowed \\
  b? \in books \\
  borrowed' \mbox{  =  } borrowed \cup { b? \mapsto p? }
  \end{schema}
  
  \begin{schema}{Return}
  \Delta Library; b? : Book; p? : Person
  \where
  b? \in \dom borrowed \\
  borrowed' \mbox{  =  } borrowed \hide { b? \mapsto p? }
  \end{schema}
  
  
  \begin{schema}{Has}
   \Xi Library; p? : Person; bks : \power Book
  \where
  bks! \mbox{  =  } borrowed ^{-1} \limg { p? } \rimg
  \end{schema}
  

slide: The library operations

Abstract systems -- design methodology
  • abstract system = abstract data types + protocol

Events -- high level glue
  • realization of the interaction protocol
slide: Abstract systems and events

Abstract system -- exemplary interface

library 



  p = new person();
  b = new book();
  p = b->borrower;
  s = p->books;
  tf = b->inlibrary();
  b->borrow(p);
  p->allocate(b);
  p->deallocate(b);
  b->_return(p);

For person* p; book* b; set<book>* s; bool tf;

slide: The library system


  class book { 
   book  

  public:
  person* borrower;
  book() {}
  void borrow( person* p ) { borrower = p;  }
  void _return( person* p ) { borrower = 0; }
  bool inlibrary() { return !borrower; }
  };
  


  class person { 
   person  

  public:
  person() { books = new set(); }
  void allocate( book* b ) { books->insert(b); }
  void deallocate( book* b ) { books->remove(b); }
  set* books;
  };
  


  book* Stroustrup = new book(); 
 example

  book* ChandyMisra = new book();
  book* Smalltalk80 = new book();
  
  person* Hans = new person();
  person* Cees = new person();
  
  Stroustrup->borrow(Hans);
  Hans->allocate(Stroustrup);
  ChandyMisra->borrow(Cees);
  Cees->allocate(ChandyMisra);
  Smalltalk80->borrow(Cees);
  Cees->allocate(Smalltalk80);
  


  class Event { 
     Event    

  public:
  virtual void operator()() = 0;
  };
  


  class Borrow : public Event { 
   Borrow  

  public:
  Borrow( person* _p, book* _b ) { _b = b; _p = p; }
  void operator()() {
  	require( _b && _p ); // _b and _p exist
  	_b->borrow(p);
  	_p->allocate(b);
  	}
  private:
  person* _p; book* _b;
  };
  


  class Return : public Event { 
   Return  

  public:
  Return( person* _p, book* _b ) { _b = b; _p = p; }
  void operator()() {
  	require( _b && _p );
  	_b->_return(p);
  	_p->deallocate(b);
          }
  private:
  person* _p; book* _b;
  };