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