001package components.map;
002
003/**
004 * {@code MapKernel} enhanced with secondary methods.
005 *
006 * @param <K>
007 *            type of {@code Map} domain (key) entries
008 * @param <V>
009 *            type of {@code Map} range (associated value) entries
010 * @mathdefinitions <pre>
011 * RANGE(
012 *   m: PARTIAL_FUNCTION
013 *  ): finite set of V satisfies
014 *  for all value: V (value is in RANGE(m) iff
015 *   there exists key: K ((key, value) is in m))
016 * </pre>
017 */
018public interface Map<K, V> extends MapKernel<K, V> {
019
020    /**
021     * A map entry (key-value pair). The only ways to obtain a reference to a
022     * map entry are from the iterator and {@code Map}'s {@code remove} and
023     * {@code removeAny} methods.
024     *
025     * @param <K>
026     *            type of {@code MapKernel} domain (key) entries
027     * @param <V>
028     *            type of {@code MapKernel} range (associated value) entries
029     * @mathmodel type Pair is modeled by (key: K, value: V)
030     * @initially <pre>
031     * (K key, V value):
032     *  ensures
033     *   this = (key, value)
034     * </pre>
035     */
036    interface Pair<K, V> {
037        /**
038         * Returns this {@code Pair}'s key.
039         *
040         * @return the key
041         * @aliases reference returned by {@code key}
042         */
043        K key();
044
045        /**
046         * Returns this {@code Pair}'s value.
047         *
048         * @return the value
049         * @aliases reference returned by {@code value}
050         */
051        V value();
052    }
053
054    /**
055     * Replaces the value associated with {@code key} in {@code this} with
056     * {@code value} and returns the old value.
057     *
058     * @param key
059     *            the key whose associated value is replaced
060     * @param value
061     *            the value replacing the old one
062     * @return the old value associated with the given key
063     * @aliases reference {@code value}
064     * @updates this
065     * @requires key is in DOMAIN(this)
066     * @ensures <pre>
067     * this = (#this \ {(key, replaceValue)}) union {(key, value)}  and
068     * (key, replaceValue) is in #this
069     * </pre>
070     */
071    V replaceValue(K key, V value);
072
073    /**
074     * Reports a key associated with {@code value} in {@code this}. Note that
075     * the key returned generally should not be changed at all via this aliased
076     * reference, and if it is then it <i>definitely must not be changed</i> in
077     * such a way that it equals another key in the map from which it was
078     * obtained.
079     *
080     * @param value
081     *            the value whose associated key is to be reported
082     * @return a key associated with value
083     * @aliases reference returned by {@code key}
084     * @requires value is in RANGE(this)
085     * @ensures (key, value) is in this
086     */
087    K key(V value);
088
089    /**
090     * Reports whether there is a pair in {@code this} whose second component is
091     * {@code value}.
092     *
093     * @param value
094     *            the value to be checked
095     * @return true iff there is a pair in {@code this} whose second component
096     *         is {@code value}
097     * @ensures hasValue = (value is in RANGE(this))
098     */
099    boolean hasValue(V value);
100
101    /**
102     * Reports whether {@code this} and {@code m} have any keys in common.
103     *
104     * @return true iff there are keys in common
105     * @param m
106     *            the {@code Map} to be checked against {@code this}
107     * @ensures sharesKeyWith = (DOMAIN(this) intersection DOMAIN(m) /= {})
108     */
109    boolean sharesKeyWith(Map<K, V> m);
110
111    /**
112     * Combines {@code m} with {@code this}.
113     *
114     * @param m
115     *            the {@code Map} to be combined with {@code this}
116     * @updates this
117     * @clears m
118     * @requires DOMAIN(this) intersection DOMAIN(m) = {}
119     * @ensures this = #this union #m
120     */
121    void combineWith(Map<K, V> m);
122
123}