| java.lang.Object
 org.jmlspecs.models.JMLValueToEqualsRelation
org.jmlspecs.models.JMLValueToEqualsMap
| JMLValueToEqualsMap | | public class JMLValueToEqualsMap extends JMLValueToEqualsRelation (Code) | | Maps (i.e., binary relations that are functional) from non-null
elements of
JMLType to non-null elements of
Object . The first type, JMLType, is called
the domain type of the map; the second type,
Object, 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
JMLValueToEqualsRelation , and as such as can be treated as a
binary relation or a set valued function also. See the
documentation for
JMLValueToEqualsRelation 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: JMLValueToEqualsRelation
See Also: JMLValueToEqualsRelationEnumerator
See Also: JMLValueToEqualsRelationImageEnumerator
See Also: JMLValueSet
See Also: JMLObjectSet
See Also: JMLObjectToObjectMap
See Also: JMLValueToObjectMap
See Also: JMLObjectToValueMap
See Also: JMLValueToValueMap
See Also: JMLValueToEqualsRelation.toFunction |
| JMLValueToEqualsMap | | protected JMLValueToEqualsMap(JMLValueSet ipset, JMLValueSet 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.
|
|
|