class bounded : public counter { 
   bounded  
  public:
  bounded(int b = MAXINT) : counter(0), max(b) {}
  void operator++() {
  	require( value() < max ); // to prevent overflow
  	counter::operator++();
  	}
  
  bool invariant() {
  	return value() <= max && counter::invariant();
  	}
  
  private:
  int max;
  };