// @(#)$Id: SmallCounter.lh,v 1.2 1998/08/27 22:56:46 leavens Exp $
// See J.P. Lejacq's paper in SIGPLAN 26(10), Oct, 1991

#include "Counter.lh"

//@ uses SmallCounterTrait;

class SmallCounter: public Counter {
public:
  //@ invariant value\any <= SmallLimit;

  SmallCounter() throw();
  //@ behavior {
  //@   modifies value;
  //@   ensures  value' = 0;
  //@ }

  virtual void increment() throw();
  //@ behavior {
  //@   requires value^ < SmallLimit;
  //@   modifies value;
  //@   ensures  value' = value^ + 1;
  //@   ensures redundantly  value' <= SmallLimit;  // by the invariant
  //@ }
};

[Index]

HTML generated using lcpp2html.