Specification of the FMap<K,V> interface type.

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

// FMap<K,V> is a Java interface type describing an abstract data type of
// immutable finite functions from keys of type K to values of type V.
//
// General restriction:  None of these methods accept null arguments.

public interface FMap<K,V> {

    // Given a key k and a value v, returns an FMap<K,V> that's just
    // like this one except the key k is associated with the value v.

    public FMap<K,V> add (K k, V v);

    // Returns true if and only if this FMap<K,V> is empty (has no keys).

    public boolean isEmpty ();

    // Returns the size (number of distinct keys) of this FMap<K,V>.

    public int size ();

    // Returns true if and only if this FMap<K,V> maps the key k to a value.

    public boolean containsKey (K k);

    // Returns the value associated with the key k in this FMap<K,V>.
    // Must not be called unless containsKey(k) is true.

    public V get (K k);
}

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

To give an algebraic specification of FMap<K,V>, we'll need a notation
for producing an empty FMap<K,V>.  In implementations of FMap<K,V>,
there's likely to be a static factory method that returns an empty
FMap<K,V>, so we'll assume the following methods are available and
return an empty FMap<K,V>:

    FMap<K,V> emptyMap ();
    FMap<K,V> emptyMap (java.util.Comparator<? super K>);

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

Algebraic specification:

    emptyMap(c) = emptyMap()

    emptyMap().isEmpty()  =  true
    m0.add(k0, v0).isEmpty()  =  false

    emptyMap().size()  =  0
    m0.add(k0, v0).size()
        =  m0.size()                           if m0.containsKey(k0)
    m0.add(k0, v0).size()
        =  1 + m0.size()                       if ! (m0.containsKey(k0))

    emptyMap().containsKey(x)  =  false
    m0.add(k0, v0).containsKey(x)
        =  true                                if x.equals(k0)
    m0.add(k0, v0).containsKey(x)
        =  m0.containsKey(x)                   if ! x.equals(k0)

    m0.add(k0, v0).get(x)
        =  v0                                  if x.equals(k0)
    m0.add(k0, v0).get(x)
        =  m0.get(x)                           if ! x.equals(k0)

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

Overriding of methods inherited from class Object.

Values of the FMap<K,V> ADT shall also implement the public
dynamic methods toString(), equals(Object), and hashCode()
consistent with the following specifications:

Specification of toString():

    m.toString() = "{...(" + m.size() + " entries)...}"

Specification of equals(Object):

    If m1 is a value of the FMap ADT, then

        m1.equals(null) returns false.

    If m1 is a value of the FMap ADT, but x is not, then

        m1.equals(x) returns false.

    If m1 and m2 are values of the FMap ADT, then
    m1.equals(m2) if and only if

    for every non-null K k

            m1.containsKey(k) if and only if m2.containsKey(k)

    and for every non-null K k

            if m1.containsKey(k)
            then m1.get(k).equals(m2.get(k))

Specification of hashCode():

    If m1 and m2 are values of the FMap ADT, and

        m1.equals(m2)

    then m1.hashCode() == m2.hashCode().

    If m1 and m2 are values of the FMap ADT, and

        ! (m1.equals(m2))

    then m1.hashCode() is unlikely to be equal to m2.hashCode().

Note:  The word "unlikely" will be interpreted as follows.
For every type K and V, if both m1 and m2 are selected at
random from a set of FMap<K,V> values such that for every
non-negative integer n and int value h the probability
of a randomly selected FMap m having n == m.size() is

    P(n) = 1/(2^(n+1))

and for each key k such that m.containsKey(k) the
probability that h == k.hashCode() is at most 1/5

and for each value v such that v.equals(m.get(k)) the
probability that h == v.hashCode() is at most 1/5

and the three probabilities above are independent

then the probability of m1.hashCode() == m2.hashCode() when
m1 and m2 are not equal is less than 40%.

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