Package components.map

Interface MapKernel<K,V>

Type Parameters:
K - type of MapKernel domain (key) entries
V - type of MapKernel range (associated value) entries
All Superinterfaces:
Iterable<Map.Pair<K,V>>, Standard<Map<K,V>>
All Known Subinterfaces:
Map<K,V>
All Known Implementing Classes:
Map1L, Map2, Map3, Map4, MapSecondary
public interface MapKernel<K,V> extends Standard<Map<K,V>>, Iterable<Map.Pair<K,V>>
Map kernel component with primary methods. (Note: by package-wide convention, all references are non-null.)
Mathematical Subtypes:
PARTIAL_FUNCTION is finite set of (key: K, value: V)
 exemplar m
 constraint
  for all key1, key2: K, value1, value2: V
    where ((key1, value1) is in m  and  (key2, value2) is in m)
   (if key1 = key2 then value1 = value2)
Mathematical Definitions:
DOMAIN(
  m: PARTIAL_FUNCTION
 ): finite set of K satisfies
 for all key: K (key is in DOMAIN(m) iff
  there exists value: V ((key, value) is in m))
Mathematical Model (abstract value and abstract invariant of this):
type MapKernel is modeled by PARTIAL_FUNCTION
Constructor(s) (initial abstract value(s) of this):
():
 ensures
  this = {}
Iterator String (abstract value of ~this):
entries(~this.seen * ~this.unseen) = this  and
|~this.seen * ~this.unseen| = |this|

  • Method Summary

    Modifier and Type
    Method
    Description
    void
    add(K key, V value)
    Adds the pair (key, value) to this.
    boolean
    hasKey(K key)
    Reports whether there is a pair in this whose first component is key.
    Map.Pair<K,V>
    remove(K key)
    Removes the pair whose first component is key and returns it.
    Map.Pair<K,V>
    removeAny()
    Removes and returns an arbitrary pair from this.
    int
    size()
    Reports size of this.
    V
    value(K key)
    Reports the value associated with key in this.

    Methods inherited from interface java.lang.Iterable

    forEach, iterator, spliterator

    Methods inherited from interface components.standard.Standard

    clear, newInstance, transferFrom

  • Method Details

    • add

      void add(K key, V value)
      Adds the pair (key, value) to this.
      Parameters:
      key - the key to be added
      value - the associated value to be added
      Aliases:
      references key, value
      Updates:
      this
      Requires:
      key is not in DOMAIN(this)
      Ensures:
      this = #this union {(key, value)}

    • remove

      Map.Pair<K,V> remove(K key)
      Removes the pair whose first component is key and returns it.
      Parameters:
      key - the key to be removed
      Returns:
      the pair removed
      Updates:
      this
      Requires:
      key is in DOMAIN(this)
      Ensures:
      remove.key = key  and
remove is in #this  and
this = #this \ {remove}

    • removeAny

      Map.Pair<K,V> removeAny()
      Removes and returns an arbitrary pair from this.
      Returns:
      the pair removed from this
      Updates:
      this
      Requires:
      |this| > 0
      Ensures:
      removeAny is in #this and
this = #this \ {removeAny}

    • value

      V value(K key)
      Reports the value associated with key in this.
      Parameters:
      key - the key whose associated value is to be reported
      Returns:
      the value associated with key
      Aliases:
      reference returned by value
      Requires:
      key is in DOMAIN(this)
      Ensures:
      (key, value) is in this

    • hasKey

      boolean hasKey(K key)
      Reports whether there is a pair in this whose first component is key.
      Parameters:
      key - the key to be checked
      Returns:
      true iff there is a pair in this whose first component is key
      Ensures:
      hasKey = (key is in DOMAIN(this))

    • size

      int size()
      Reports size of this.
      Returns:
      the number of pairs in this
      Ensures:
      size = |this|