| Method Summary |
|
| public JMLValueToValueRelation | add(JMLType dv, JMLType rv)
Return a relation that is just like this relation, except that
it also associates the given domain element to the given range
element. |
| public JMLValueToValueRelationEnumerator | associations()
Return a enumerator for the set of associations that
conceptually make up this relation. |
| public Object | clone()
Return a clone of this object. |
| public JMLValueToValueRelation | compose(JMLValueToValueRelation othRel)
Return a relation that is the composition of the given
relation and this relation. |
| public JMLObjectToValueRelation | compose(JMLObjectToValueRelation othRel)
Return a relation that is the composition of the given
relation and this relation. |
| public JMLValueToValueRelation | difference(JMLValueToValueRelation othRel)
Return a relation that is the difference between this and the given
relation. |
| public JMLValueSet | domain()
Returns a set containing the domain of this relation. |
| public JMLValueSetEnumerator | domainElements()
Return a enumerator for the set that is the domain of this
relation. |
| public JMLValueSet | elementImage(JMLType dv)
Returns a set containing all the range elements that this
relation relates to the given domain element. |
| public JMLValueToValueRelationEnumerator | elements()
Return a enumerator for the set of associations that
conceptually make up this relation. |
| public boolean | equals(Object obj)
Test whether this object's value is equal to the given argument. |
| public boolean | has(JMLType dv, JMLType rv)
Tells whether this associates the given key to the given value. |
| public boolean | has(JMLValueValuePair pair)
Tells whether this associates the given key to the given value. |
| public boolean | has(Object obj)
Tells whether this associates the given key to the given value. |
| public int | hashCode()
Return a hash code for this object. |
| public JMLValueSet | image(JMLValueSet dom)
Returns a set containing all the range elements that this
relation relates to the elements of the given set of domain elements. |
| public JMLValueSet | imagePairSet()
Return the set of image set pairs that make up this relation. |
| public JMLValueToValueRelationImageEnumerator | imagePairs()
Return the set of domain image set pairs that make up this relation. |
| public JMLValueToValueRelation | insert(JMLValueValuePair pair)
Return a relation that is just like this relation, except that
it also includes the association described by the given pair. |
| public int | int_size()
Return the number of associations in this relation. |
| public JMLValueToValueRelation | intersection(JMLValueToValueRelation othRel)
Return a relation that is the intersection of this and the
given relation. |
| public JMLValueToValueRelation | inverse()
Returns the inverse of this relation. |
| public JMLValueSet | inverseElementImage(JMLType rv)
Return a set of all the domain elements that relate to the
given range element. |
| public JMLValueSet | inverseImage(JMLValueSet rng)
Return a set of all the domain elements that relate to some
element in the given set of range elements. |
| public boolean | isDefinedAt(JMLType dv)
Tells whether this relation associates any range element to the
given domain element. |
| public boolean | isEmpty()
Tells whether the relation is empty. |
| public boolean | isaFunction()
Tells whether this relation is a function. |
| public JMLIterator | iterator()
Returns an Iterator over the set of pairs conceptually
contained in this relation.. |
| public JMLValueSet | range()
Returns a set containing the range of this relation. |
| public JMLValueSetEnumerator | rangeElements()
Return a enumerator for the set that is the range of this
relation. |
| public JMLValueToValueRelation | remove(JMLType dv, JMLType rv)
Return a relation that is just like this relation, except that
it does not contain the association, if any, between the given
domain and range elements. |
| public JMLValueToValueRelation | remove(JMLValueValuePair pair)
Return a relation that is just like this relation, except that
it does not contain association described by the given pair. |
| public JMLValueToValueRelation | removeFromDomain(JMLType dv)
Return a relation that is just like this relation, except that
it does not contain any association with the given domain element. |
| public JMLValueToValueRelation | restrictDomainTo(JMLValueSet dom)
Return a relation that is like this relation except that its
domain is limited to just the elements of the given set. |
| public JMLValueToValueRelation | restrictRangeTo(JMLValueSet rng)
Return a relation that is like this relation except that its
range is limited to just the elements of the given set. |
| public static JMLValueToValueRelation | singleton(JMLType dv, JMLType rv)
Return the singleton relation containing the given association. |
| public static JMLValueToValueRelation | singleton(JMLValueValuePair pair)
Return the singleton relation containing the association
described by the given pair. |
| public JMLValueBag | toBag()
Return the bag of all associations in this relation. |
| public JMLValueToValueMap | toFunction()
Return a map that is contained in this relation. |
| public JMLValueSequence | toSequence()
Return a sequence containing all associations in this relation. |
| public JMLValueSet | toSet()
Return the set of all associations in this relation. |
| public String | toString()
Return a string representation of this object. |
| public JMLValueToValueRelation | union(JMLValueToValueRelation othRel)
Return a relation that union of the this and the given relation. |
