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


  };