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 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 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|
-