Package components.map
Interface MapKernel<K,V>
 Type Parameters:
K
 type ofMapKernel
domain (key) entriesV
 type ofMapKernel
range (associated value) entries
 All Known Subinterfaces:
Map<K,
V>
 All Known Implementing Classes:
Map1L
,Map2
,Map3
,Map4
,MapSecondary
Map kernel component with primary methods. (Note: by packagewide convention,
all references are nonnull.)
 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 TypeMethodDescriptionvoid
Adds the pair (key
,value
) to this.boolean
Reports whether there is a pair inthis
whose first component iskey
.Removes the pair whose first component iskey
and returns it.Removes and returns an arbitrary pair fromthis
.int
size()
Reports size ofthis
.Reports the value associated withkey
inthis
.Methods inherited from interface java.lang.Iterable
forEach, iterator, spliterator
Methods inherited from interface components.standard.Standard
clear, newInstance, transferFrom

Method Details

add
Adds the pair (key
,value
) to this. Parameters:
key
 the key to be addedvalue
 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
Removes the pair whose first component iskey
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
Removes and returns an arbitrary pair fromthis
. Returns:
 the pair removed from
this
 Updates:
this
 Requires:
this > 0
 Ensures:
removeAny is in #this and this = #this \ {removeAny}

value
Reports the value associated withkey
inthis
. 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
Reports whether there is a pair inthis
whose first component iskey
. 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 ofthis
. Returns:
 the number of pairs in
this
 Ensures:
size = this
