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