class counter { 
   counter  
  public:
  counter(int n = 0) : _n(n) {
  	require( n >= 0 );
  	promise( invariant() ); 
 check initial state
  	}
  
  virtual void operator++() {
  	require( true ); 
 empty pre-condition
  	hold(); 
 save the previous state
  	_n += 1;
  	promise( _n == old_n + 1 && invariant() );
  	}
  
  int value() const { return _n; }  
 no side effects
  
  virtual bool invariant() { return value() >= 0; }
  
  protected:
  int _n;
  int old_n;
  virtual void hold() { old_n = n; }
  };