package counters; /** * * Implements a simple counter value whose current value is an * an integer and a positive integer limit that is specified * when the counter is created. *
* *

* Class Invariant: *

*
    *
  1. limit is a positive integer that can be * represented exactly using Java’s int * data type *
  2. *
  3. value is an integer whose value is between * 0 and limit−1 (inclusive) *
  4. *
* * @author Wayne Eberly * */ public class SimpleCounter implements Counter { // Data Fields /** Upper bound on the counter value */ private final int limit; /** Current counter value */ private int value; // Constructor /** * * Constructor method using a given value for the counter’s * limit. *

* * Precondition 1: *
    *
  1. inLimit is a postive integer.
  2. *

* * Postcondition 1: *
    *
  1. A new instance of this class is created. The * limit of this new object is * equal to the given value inLimit * and the value for this new object * is equal to zero.
  2. *

* * Precondition 2: *
    *
  1. inLimit is an integer that is less than or equal to zero.
  2. *

* * Postconditions 2: *
    *
  1. A new instance of this class is not created.
  2. *
  3. An IllegalArgumentException is thrown.
  4. *
* * @param inLimit The limit of the object to be created * @throws IllegalArgumentException if the input is less than * or equal to zero */ public SimpleCounter(int inLimit) { if (inLimit < 1) { throw new IllegalArgumentException("Negative or zero counter limit: " + inLimit); } else { limit = inLimit; value = 0; }; }; // Accessor Methods /** * * 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 class invariant * is also satisfied on termination.
  2. *
  3. The value returned is equal to this counter’s * limit
  4. *
* * @return The limit of this counter * */ public int getLimit () { return this.limit; }; /** * * Accessor method used to display the counter’s * current value. *

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

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

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

* * 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. *
  3. 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)
  4. *

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

* * 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. *
  3. limit = 0.
  4. *
  5. A LimitReachedException is thrown.
  6. *
* * @throws LimitReachedException if the value is at * its maximal value when this method is applied * */ public void advanceValue () throws LimitReachedException { this.value++; if (this.value == this.limit) { this.value = 0; throw new LimitReachedException("Counter value reset."); }; }; }