Contracts

For dynamically checking the invariance condition, a test should be executed when evaluating the constructor and before and after each method invocation. While a method is being executed, the invariant need not necessarily hold, but it is the responsibility of a method to restore the invariant when it is disrupted. In case object methods are recursively applied, the invariant must be restored when returning to the original caller.

An alternative approach to incorporating assertions in a class description is presented in  [Cline], which introduces an extension of C++ called Annotated C++. Instead of directly embedding assertions in the code, Annotated C++ requires the user to specify separately the axioms characterizing the functionality of the methods and their effect on the state of the object.

Interfaces

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

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

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

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