// @(#)$Id: SmallCounterDesugared.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 <= Limit   // inherited
  //@          /\ value\any <= SmallLimit;

  //@ constraint value\pre <= value\post;   // inherited


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

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

[Index]

HTML generated using lcpp2html.