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

slide: Refining the counter contract