001package components.map;
002
003import components.standard.Standard;
004
005/**
006 * Map kernel component with primary methods. (Note: by package-wide convention,
007 * all references are non-null.)
008 *
009 * @param <K>
010 *            type of {@code MapKernel} domain (key) entries
011 * @param <V>
012 *            type of {@code MapKernel} range (associated value) entries
013 * @mathsubtypes <pre>
014 * PARTIAL_FUNCTION is finite set of (key: K, value: V)
015 *  exemplar m
016 *  constraint
017 *   for all key1, key2: K, value1, value2: V
018 *     where ((key1, value1) is in m  and  (key2, value2) is in m)
019 *    (if key1 = key2 then value1 = value2)
020 * </pre>
021 * @mathdefinitions <pre>
022 * DOMAIN(
023 *   m: PARTIAL_FUNCTION
024 *  ): finite set of K satisfies
025 *  for all key: K (key is in DOMAIN(m) iff
026 *   there exists value: V ((key, value) is in m))
027 * </pre>
028 * @mathmodel type MapKernel is modeled by PARTIAL_FUNCTION
029 * @initially <pre>
030 * ():
031 *  ensures
032 *   this = {}
033 * </pre>
034 * @iterator <pre>
035 * entries(~this.seen * ~this.unseen) = this  and
036 * |~this.seen * ~this.unseen| = |this|
037 * </pre>
038 */
039public interface MapKernel<K, V> extends Standard<Map<K, V>>, Iterable<Map.Pair<K, V>> {
040
041    /**
042     * Adds the pair ({@code key}, {@code value}) to this.
043     *
044     * @param key
045     *            the key to be added
046     * @param value
047     *            the associated value to be added
048     * @aliases references {@code key, value}
049     * @updates this
050     * @requires key is not in DOMAIN(this)
051     * @ensures this = #this union {(key, value)}
052     */
053    void add(K key, V value);
054
055    /**
056     * Removes the pair whose first component is {@code key} and returns it.
057     *
058     * @param key
059     *            the key to be removed
060     * @return the pair removed
061     * @updates this
062     * @requires key is in DOMAIN(this)
063     * @ensures <pre>
064     * remove.key = key  and
065     * remove is in #this  and
066     * this = #this \ {remove}
067     * </pre>
068     */
069    Map.Pair<K, V> remove(K key);
070
071    /**
072     * Removes and returns an arbitrary pair from {@code this}.
073     *
074     * @return the pair removed from {@code this}
075     * @updates this
076     * @requires |this| > 0
077     * @ensures <pre>
078     * removeAny is in #this and
079     * this = #this \ {removeAny}
080     * </pre>
081     */
082    Map.Pair<K, V> removeAny();
083
084    /**
085     * Reports the value associated with {@code key} in {@code this}.
086     *
087     * @param key
088     *            the key whose associated value is to be reported
089     * @return the value associated with key
090     * @aliases reference returned by {@code value}
091     * @requires key is in DOMAIN(this)
092     * @ensures (key, value) is in this
093     */
094    V value(K key);
095
096    /**
097     * Reports whether there is a pair in {@code this} whose first component is
098     * {@code key}.
099     *
100     * @param key
101     *            the key to be checked
102     * @return true iff there is a pair in this whose first component is
103     *         {@code key}
104     * @ensures hasKey = (key is in DOMAIN(this))
105     */
106    boolean hasKey(K key);
107
108    /**
109     * Reports size of {@code this}.
110     *
111     * @return the number of pairs in {@code this}
112     * @ensures size = |this|
113     */
114    int size();
115
116}