package counters; /** * * Provides a counter interface. *
* *

* Interface Invariant: *

*
    *
  1. limit is a positive integer that can be * represented exactly using Java’s int * data type *
    2. *
  2. value is an integer whose value is between * 0 and limit−1 (inclusive) *
    3. *
* *

* Additional Notes: *

* *

* A constructor should be provided that allows a counter with * a given positive integer limit to be created. * The default initial valuex should be zero. *

* */ public interface Counter { /** * * Accessor method used to display the value of the * counter’s limit. *

* * Precondition: *
    *
  1. The class invariant is satisfied.
    2. *

* * Postcondition: *
    *
  1. The object is not changed (so that the interface invariant * is also satisfied on termination).
    2. *
  2. The value returned is equal to this counter’s * limit
    3. *
* * @return The limit of this counter * */ int getLimit (); /** * * Accessor method used to display the counter’s * current value. *

* * Precondition: *
    *
  1. The interface invariant is satisfied.
    2. *

* * Postcondition: *
    *
  1. The object is not changed (so that the class invariant * is also satisfied on termination).
    2. *
  2. The value returned is equal to this counter’s * value
    3. *
* * @return The current value of this counter * */ int getValue (); // Mutator Method /** * * Mutator method to increment the counter’s * value. *

* * Precondition 1: *
    *
  1. The interface invariant is satisfied.
    2. *
  2. value < limit−1
    3. *

* * Postcondition 1: *
    *
  1. The object’s limit is not changed * (so that it is still a postive integer that can be * represented exactly using Java’s int * data type).
    2. *
  2. If the initial value of value is v, then * the final value is equal to v+1 * (which is an integer between 0 * and limit−1, as required)
    3. *

* * Precondition 2: *
    *
  1. The interface invariant is satisfied.
    2. *
  2. value = limit−1
    3. *

* * Postcondition 2: *
    *
  1. The object’s limit is not changed * (so that it is still a positive integer that can be * represented exactly using Java’s int * data type).
    2. *
  2. limit = 0.
    3. *
  3. A LimitReachedException is thrown.
    4. *
* * @throws LimitReachedException if the value is at * its maximal value when this method is applied * */ public void advanceValue () throws LimitReachedException; }