There have been a few changes from the specification used
for assignment 1.  Changes are marked by a # in column 79.

--------------------------------------------------

Specification of the Refreshable ADT.

The Refreshable ADT shall be implemented in Java, and will be tested
using Sun's Java 2 Runtime Environment, Standard Edition, version 1.6.0.
The code for this implementation will be in the default package, and
shall define a public class named Refreshable.  That class shall
provide the following public static methods:

Signature:

    Refreshable.create : String * long -> Refreshable                         #
    Refreshable.name   : Refreshable  -> String
    Refreshable.era    : Refreshable  -> long

    Refreshable.name (Refreshable.create (s, i)) = s

    Refreshable.era (Refreshable.create (s, i)) = i

Note: The second argument to Refreshable.create must be greater
than or equal to 0.  If this constraint is violated, then an
IllegalArgument exception should be thrown, as by the following
statement:

      throw new IllegalArgumentException("era < 0");

Values of the Refreshable ADT shall also implement the public
dynamic methods equals(Object) and hashCode() such that

    If v1 and v2 are values of the Refreshable ADT, then

        v1.equals(v2) if and only if
            v1 == v2                                                          #

    If v1 is a value of the Refreshable ADT, but x is not, then

        v1.equals(x) returns false.

    If v1 and v2 are values of the Refreshable ADT, and

        v1.equals(v2)

    then v1.hashCode() == v2.hashCode().

Note: The value returned by hashCode() must not change when the               #
refresh(long) method, described below, is used.                               #

Values of the Refreshable ADT shall also implement the public                 #
dynamic methods void refresh(long) such that                                  #
                                                                              #
    If v is a value of the Refreshable ADT, and                               #
    Refreshable.era(v) >= j, then v.refresh(j) does nothing.                  #
                                                                              #
    If v is a value of the Refreshable ADT, and                               #
    Refreshable.era(v) < j, then v.refresh(j) changes the                     #
    state of v so that subsequent calls to Refreshable.era(v)                 #
    will return j.                                                            #

--------------------------------------------------