| java.lang.Object
 org.jmlspecs.models.JMLEqualsToValueRelation
org.jmlspecs.models.JMLEqualsToValueMap
| JMLEqualsToValueMap | | public class JMLEqualsToValueMap extends JMLEqualsToValueRelation (Code) | | Maps (i.e., binary relations that are functional) from non-null
elements of
Object to non-null elements of
JMLType . The first type, Object, is called
the domain type of the map; the second type,
JMLType, 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
JMLEqualsToValueRelation , and as such as can be treated as a
binary relation or a set valued function also. See the
documentation for
JMLEqualsToValueRelation 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: JMLEqualsToValueRelation
See Also: JMLEqualsToValueRelationEnumerator
See Also: JMLEqualsToValueRelationImageEnumerator
See Also: JMLValueSet
See Also: JMLObjectSet
See Also: JMLObjectToObjectMap
See Also: JMLValueToObjectMap
See Also: JMLObjectToValueMap
See Also: JMLValueToValueMap
See Also: JMLEqualsToValueRelation.toFunction |
| JMLEqualsToValueMap | | protected JMLEqualsToValueMap(JMLValueSet ipset, JMLEqualsSet dom, int sz)(Code) | | Initialize this map based on the representation values given.
|
| isaFunction | | public boolean isaFunction()(Code) | | Tells whether this relation is a function.
|
|
|