subsections:

Assertions -- formal specification

slide: Formal specification of contracts

slide: The substitutability requirement
 

  class account {  
   account  

  public:
  account();
  // assert( invariant() );
  
  virtual float balance() { return _balance; }
  
  void deposit(float x); 
 to deposit money

  // require( x >= 0 );
  // promise( balance()  ==  old_balance  +  x  && invariant() );
  
  void withdraw(float x); 
 to withdraw money

  // require( x  <=  balance() );
  // promise( balance()  ==  old_balance  -  x && invariant() );
  
  bool invariant() { return balance()  >=  0; }
  protected:
  float _balance;
  };
slide: The $account$ contract

System development

A pre-condition limits the cases that a supplier must handle!

slide: System development with contracts
 

  class account { 
   account  

  public:
  account() { _balance = 0; assert(invariant()); }
  
  virtual float balance() { return _balance; }
  
  
  void deposit(float x) {
  	require( x >= 0 );  // check precondition
  	hold(); // to save the old state
  	_balance += x; 
  	promise( balance() == old_balance + x );
  	promise( invariant() );
  	}
  
  void withdraw(float x) {
  	require( x <= _balance );  // check precondition
  	hold(); // to save the old state
  	_balance -= x; 
  	promise( balance() == old_balance - x );
  	promise( invariant() );
  	}
  
  virtual bool invariant() { return balance() >= 0; }
  protected:
  float _balance;
  float old_balance; // additional variable
  virtual void hold() { old_balance = _balance; }
  };
slide: The realization of the $account$ contract

Refining a contract -- state responsibilities and obligations

  • invariance -- respect the invariants of the base class
  • methods -- services may be added or refined

Refining a method -- like improving a business contract


  class C : public P {
  	virtual void m();
  	}

  • pre(m_C) >= pre(m_P)


  • post(m_C) <= post(m_P)


slide: Contracts and inheritance
 

  class credit_account : public account { 
   credit_account  

  public:
  credit_account(float x) { _maxcredit = x; _credit = 0; }
  
  float balance() { return _balance + _credit; }
  
  float credit(float x) { 
  	require( x + _credit <= _maxcredit );
  	hold();
  	_credit += x;
  	promise( _credit = old_credit + x );
  	promise( _balance = old_balance);
  	promise( invariant() );
  	}
  
  void reduce(float x) {
  	require( 0 <= x && x <= _credit );
  	hold();
  	_credit -= x;
  	promise( _credit = old_credit - x );
  	promise( _balance = old_balance );
  	promise( invariant() );
  	}
  
  
  bool invariant() {
  	return _credit <= _maxcredit && account::invariant();
  	}
  protected:
  float _maxcredit, _credit;
  float old_credit;
  void hold() { old_credit = _credit; account::hold(); }
  };
slide: Refining the account contract

Assertions -- side-effect free

contracts


  • require -- test on delivery
  • promise -- test during development

Object invariance -- exceptions

  • invariant -- verify when needed

Global properties -- requirements

  • interaction protocols -- formal specification
slide: Runtime consistency checking