The account contract

introduction teaching contracts patterns events examples foundations conclusions references

An ordinary account supports methods to deposit and withdraw money and allows for inquiring after the balance as well. As an invariant of an ordinary account we may assume that the balance must be equal to or greater than zero. The account class below gives an example of how to realize a contract in C++ code.

The account class

  class account {
  public:
  account() { _balance = 0; promise(account::invariant()); }
   
  virtual float balance() const { return _balance; }
   
   
  void deposit(float x) {
          require( x >= 0 );   check precondition


          hold();  to save the old state


          _balance += x; 
          promise( balance() == old_balance + x && invariant() );
          }
   
  void withdraw(float x) {
          require( x <= balance() );   check precondition


          hold();  to save the old state


          _balance -= x; 
          promise( balance() == old_balance - x && invariant() );
          }
   
  protected:
     virtual bool invariant() { return balance() >= 0; }
     virtual void hold() { old_balance = balance(); }
  private:
     float _balance;
     float old_balance;  additional variable


  };

slide: The account class

Pre- and post-conditions are realized by calling respectively the require and promise macros, which are simply variants of the C assert macro. To check whether the post-conditions for (state-changing) methods are satisfied, a virtual function hold is introduced that copies the value of (selected parts of) the state of the object. We use the prefix old to indicate these additional instance variables. To check whether a contract is satisfied runtime, we must test that the invariant is satisfied when the object is created. Further, when a method is invoked, we must test its pre-condition and establish that its post-condition is satisfied and that the object invariance is not violated.

A credit_account may be considered to be an improvement over an ordinary account since it allows us to draw more money from it. One possible realization is given below.

  class credit_account : public account {
  public:
  credit_account(float x) { _maxcredit = x; _credit = 0; }
  
  float balance() { return _balance + _credit; }
  
  float credit(float x) { 
  	require( x >= 0 && x + _credit <= _maxcredit );
  	hold();
  	_credit += x;
  	promise( _credit = old_credit + x );
  	promise( balance() == old_balance + x && invariant() );
  	}
  
  
  protected:
    bool invariant() {
  	  return _credit <= _maxcredit && account::invariant();
  	  }
    void hold() { old_credit = _credit; account::hold(); }
  private:
    float _maxcredit, _credit;
    float old_credit;
  };

We merely introduce one additional method to raise the credit, and extend the function hold to keep track of the _credit variable. Note that the invariant is indeed strengthened and that the pre-condition of withdraw has (implicitly) been weakened. An alternative solution would consist of redefining deposit and withdraw. This is left as an exercise.