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