| org.jmlspecs.models.JML_Domain_To_Range_Map
| JML_Domain_To_Range_Map | | public class JML_Domain_To_Range_Map extends JML_Domain_To_Range_Relation (Code) | | Maps (i.e., binary relations that are functional) from non-null
elements of
_DomainType_ to non-null elements of
_RangeType_ . The first type, _DomainType_, is called
the domain type of the map; the second type,
_RangeType_, is called the range type of the map. A
map can be seen as a set of pairs, of form (dv, rv),
consisting of an element of the domain type, dv, and an
element of the range type, rv. Alternatively, it can be
seen as a function that maps each element of the domain to some of
elements of the range type.
This type is a subtype of
JML_Domain_To_Range_Relation , and as such as can be treated as a
binary relation or a set valued function also. See the
documentation for
JML_Domain_To_Range_Relation and for the
methods inherited from this supertype for more information.
This type considers elements val and dv
of the domain type, to be distinct just when
_val_not_equal_to_dv_. It considers elements of
r and rv of the range type to be distinct
just when _r_not_equal_to_rv_. Cloning takes place for
the domain or range elements if the corresponding domain or range
type is
JMLType .
version:
$Revision: 1.2 $
author:
Gary T. Leavens
author:
Clyde Ruby
See Also: JMLCollection
See Also: JMLType
See Also: JML_Domain_To_Range_Relation
See Also: JML_Domain_To_Range_RelationEnumerator
See Also: JML_Domain_To_Range_RelationImageEnumerator
See Also: JMLValueSet
See Also: JMLObjectSet
See Also: JMLObjectToObjectMap
See Also: JMLValueToObjectMap
See Also: JMLObjectToValueMap
See Also: JMLValueToValueMap
See Also: JML_Domain_To_Range_Relation.toFunction |
| Field Summary | |
| final public static JML_Domain_To_Range_Map | EMPTY
The empty JML_Domain_To_Range_Map. |
| Constructor Summary | |
| public | JML_Domain_To_Range_Map()
Initialize this map to be the empty mapping. | | public | JML_Domain_To_Range_Map(_DomainType_ dv, _RangeType_ rv)
Initialize this map to be a mapping that maps the given domain
element to the given range element. | | public | JML_Domain_To_Range_Map(JML_Domain__Range_Pair pair)
Initialize this map to be a mapping that maps the key in the
given pair to the value in that pair. | | protected | JML_Domain_To_Range_Map(JMLValueSet ipset, JML_Domain_Set dom, int sz)
Initialize this map based on the representation values given. |
| Method Summary | |
| public _RangeType_ | apply(_DomainType_ dv)
Return the range element corresponding to dv, if there is one. | | public JML_Domain_To_Range_Map | clashReplaceUnion(JML_Domain_To_Range_Map othMap, _RangeType_ errval)
Return a new map that is like the union of the given map and
this map, except that if both define a mapping for a given
domain element, then each of these clashes is replaced by a
mapping from the domain element in question to the given range
element. | | public Object | clone()
| | public JMLValueTo_Range_Map | compose(JMLValueTo_Domain_Map othMap)
Return a new map that is the composition of this and the given
map. | | public JMLObjectTo_Range_Map | compose(JMLObjectTo_Domain_Map othMap)
Return a new map that is the composition of this and the given
map. | | public JML_Domain_To_Range_Map | disjointUnion(JML_Domain_To_Range_Map othMap)
Return a map that is the disjoint union of this and othMap. | | public JML_Domain_To_Range_Map | extend(_DomainType_ dv, _RangeType_ rv)
Return a new map that is like this but maps the given domain
element to the given range element. | | public JML_Domain_To_Range_Map | extendUnion(JML_Domain_To_Range_Map othMap)
Return a new map that is like the union of the given map and
this map, except that if both define a mapping for a given domain
element, then only the mapping in the given map is retained. | | public boolean | isaFunction()
Tells whether this relation is a function. | | public JML_Domain_To_Range_Map | rangeRestrictedTo(JML_Range_Set rng)
Return a new map that is like this map but only contains
associations that map to range elements in the given set. | | public JML_Domain_To_Range_Map | removeDomainElement(_DomainType_ dv)
Return a new map that is like this but has no association for the
given domain element. | | public JML_Domain_To_Range_Map | restrictedTo(JML_Domain_Set dom)
Return a new map that only maps elements in the given domain
to the corresponding range elements in this map. | | public static JML_Domain_To_Range_Map | singletonMap(_DomainType_ dv, _RangeType_ rv)
Return the singleton map containing the given association. | | public static JML_Domain_To_Range_Map | singletonMap(JML_Domain__Range_Pair pair)
Return the singleton map containing the association described
by the given pair. |
| EMPTY | | final public static JML_Domain_To_Range_Map EMPTY(Code) | | The empty JML_Domain_To_Range_Map.
See Also: JML_Domain_To_Range_Map.JML_Domain_To_Range_Map() |
| JML_Domain_To_Range_Map | | public JML_Domain_To_Range_Map()(Code) | | Initialize this map to be the empty mapping.
See Also: JML_Domain_To_Range_Map.EMPTY |
| JML_Domain_To_Range_Map | | public JML_Domain_To_Range_Map(_DomainType_ dv, _RangeType_ rv)(Code) | | Initialize this map to be a mapping that maps the given domain
element to the given range element.
See Also: JML_Domain_To_Range_Map.singletonMap(_DomainType_,_RangeType_)
See Also: JML_Domain_To_Range_Map.JML_Domain_To_Range_Map(JML_Domain__Range_Pair) |
| JML_Domain_To_Range_Map | | public JML_Domain_To_Range_Map(JML_Domain__Range_Pair pair)(Code) | | Initialize this map to be a mapping that maps the key in the
given pair to the value in that pair.
See Also: JML_Domain_To_Range_Map.singletonMap(JML_Domain__Range_Pair)
See Also: JML_Domain_To_Range_Map.JML_Domain_To_Range_Map(_DomainType_,_RangeType_) |
| JML_Domain_To_Range_Map | | protected JML_Domain_To_Range_Map(JMLValueSet ipset, JML_Domain_Set dom, int sz)(Code) | | Initialize this map based on the representation values given.
|
| apply | | public _RangeType_ apply(_DomainType_ dv) throws JMLNoSuchElementException(Code) | | Return the range element corresponding to dv, if there is one.
Parameters:
dv - the domain element for which an association issought (the key to the table).
exception:
JMLNoSuchElementException - when dv is not associatedto any range element by this.
See Also: JML_Domain_To_Range_Relation.isDefinedAt
See Also: JML_Domain_To_Range_Relation.elementImage
See Also: JML_Domain_To_Range_Relation.image |
| clashReplaceUnion | | public JML_Domain_To_Range_Map clashReplaceUnion(JML_Domain_To_Range_Map othMap, _RangeType_ errval) throws IllegalStateException(Code) | | Return a new map that is like the union of the given map and
this map, except that if both define a mapping for a given
domain element, then each of these clashes is replaced by a
mapping from the domain element in question to the given range
element.
Parameters:
othMap - the other map.
Parameters:
errval - the range element to use when clashes occur.
See Also: JML_Domain_To_Range_Map.extendUnion
See Also: JML_Domain_To_Range_Map.disjointUnion
See Also: JML_Domain_To_Range_Relation.union |
| compose | | public JMLValueTo_Range_Map compose(JMLValueTo_Domain_Map othMap)(Code) | | Return a new map that is the composition of this and the given
map. The composition is done in the usual order; that is, if
the given map maps x to y and this maps y to z, then the
result maps x to z.
See Also: JML_Domain_To_Range_Map.compose(JMLObjectTo_Domain_Map) |
| compose | | public JMLObjectTo_Range_Map compose(JMLObjectTo_Domain_Map othMap)(Code) | | Return a new map that is the composition of this and the given
map. The composition is done in the usual order; that is, if
the given map maps x to y and this maps y to z, then the
result maps x to z.
See Also: JML_Domain_To_Range_Map.compose(JMLValueTo_Domain_Map) |
| disjointUnion | | public JML_Domain_To_Range_Map disjointUnion(JML_Domain_To_Range_Map othMap) throws JMLMapException, IllegalStateException(Code) | | Return a map that is the disjoint union of this and othMap.
Parameters:
othMap - the other mapping
exception:
JMLMapException - the ranges of this and othMap have elementsin common (i.e., when they interesect).
See Also: JML_Domain_To_Range_Map.extendUnion
See Also: JML_Domain_To_Range_Map.clashReplaceUnion
See Also: JML_Domain_To_Range_Relation.union |
| extend | | public JML_Domain_To_Range_Map extend(_DomainType_ dv, _RangeType_ rv)(Code) | | Return a new map that is like this but maps the given domain
element to the given range element. Any previously existing
mapping for the domain element is removed first.
See Also: JML_Domain_To_Range_Relation.insert(_DomainType__RangeType_) |
| extendUnion | | public JML_Domain_To_Range_Map extendUnion(JML_Domain_To_Range_Map othMap) throws IllegalStateException(Code) | | Return a new map that is like the union of the given map and
this map, except that if both define a mapping for a given domain
element, then only the mapping in the given map is retained.
See Also: JML_Domain_To_Range_Map.clashReplaceUnion
See Also: JML_Domain_To_Range_Map.disjointUnion
See Also: JML_Domain_To_Range_Relation.union |
| isaFunction | | public boolean isaFunction()(Code) | | Tells whether this relation is a function.
|
| rangeRestrictedTo | | public JML_Domain_To_Range_Map rangeRestrictedTo(JML_Range_Set rng)(Code) | | Return a new map that is like this map but only contains
associations that map to range elements in the given set.
See Also: JML_Domain_To_Range_Map.restrictedTo
See Also: JML_Domain_To_Range_Relation.restrictRangeTo |
| removeDomainElement | | public JML_Domain_To_Range_Map removeDomainElement(_DomainType_ dv)(Code) | | Return a new map that is like this but has no association for the
given domain element.
See Also: JML_Domain_To_Range_Relation.removeFromDomain |
| restrictedTo | | public JML_Domain_To_Range_Map restrictedTo(JML_Domain_Set dom)(Code) | | Return a new map that only maps elements in the given domain
to the corresponding range elements in this map.
See Also: JML_Domain_To_Range_Map.rangeRestrictedTo
See Also: JML_Domain_To_Range_Relation.restrictDomainTo |
| singletonMap | | public static JML_Domain_To_Range_Map singletonMap(_DomainType_ dv, _RangeType_ rv)(Code) | | Return the singleton map containing the given association.
See Also: JML_Domain_To_Range_Map.JML_Domain_To_Range_Map(_DomainType_,_RangeType_)
See Also: JML_Domain_To_Range_Map.singletonMap(JML_Domain__Range_Pair) |
| singletonMap | | public static JML_Domain_To_Range_Map singletonMap(JML_Domain__Range_Pair pair)(Code) | | Return the singleton map containing the association described
by the given pair.
See Also: JML_Domain_To_Range_Map.JML_Domain_To_Range_Map(JML_Domain__Range_Pair)
See Also: JML_Domain_To_Range_Map.singletonMap(_DomainType_,_RangeType_) |
|
|