JML

org.jmlspecs.models
Class JMLValueToEqualsRelation

java.lang.Object
  extended byorg.jmlspecs.models.JMLValueToEqualsRelation
All Implemented Interfaces:
Cloneable, JMLCollection, JMLType, Serializable
Direct Known Subclasses:
JMLValueToEqualsMap

public class JMLValueToEqualsRelation
extends Object
implements JMLCollection

Binary relations (or set-valued functions) from non-null elements of JMLType to non-null elements of Object. The first type, JMLType, is called the domain type of the relation; the second type, Object, is called the range type of the relation. A relation 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 set-valued function that relates each element of the domain type to some set of elements of the range type (a JMLEqualsSet).

This type considers elements val and dv of the domain type, to be distinct just when !val.equals(dv). It considers elements of r and rv of the range type to be distinct just when !r.equals(rv). Cloning takes place for the domain or range elements if the corresponding domain or range type is JMLType.

Version:
$Revision: 1.52 $
Author:
Gary T. Leavens, Clyde Ruby
See Also:
JMLCollection, JMLType, JMLValueToEqualsMap, JMLValueToEqualsRelationEnumerator, JMLValueToEqualsRelationImageEnumerator, JMLValueSet, JMLObjectSet, JMLObjectToObjectRelation, JMLValueToObjectRelation, JMLObjectToValueRelation, JMLValueToValueRelation

Field Summary
protected  JMLValueSet domain_
          The set of pairs of keys and values conceptually contained in this object.
static JMLValueToEqualsRelation EMPTY
          The empty JMLValueToEqualsRelation.
protected  JMLValueSet imagePairSet_
          The set representing the image pairs in the relation.
protected  int size_
          The size (number of pairs) of this relation.
private static String TOO_BIG_TO_INSERT
           
protected static String TOO_BIG_TO_UNION
           
 
Constructor Summary
  JMLValueToEqualsRelation()
          Initialize this to be an empty relation.
  JMLValueToEqualsRelation(JMLType dv, Object rv)
          Initialize this to be a relation containing a single association between the given domain and range elements.
  JMLValueToEqualsRelation(JMLValueEqualsPair pair)
          Initialize this to be a relation containing a single association given by the pair.
protected JMLValueToEqualsRelation(JMLValueSet ipset, JMLValueSet dom, int sz)
          Initialize this using the given representation.
 
Method Summary
 JMLValueToEqualsRelation add(JMLType dv, Object rv)
          Return a relation that is just like this relation, except that it also associates the given domain element to the given range element.
 JMLValueToEqualsRelationEnumerator associations()
          Return a enumerator for the set of associations that conceptually make up this relation.
 Object clone()
          Return a clone of this object.
 JMLObjectToEqualsRelation compose(JMLObjectToValueRelation othRel)
          Return a relation that is the composition of the given relation and this relation.
 JMLValueToEqualsRelation compose(JMLValueToValueRelation othRel)
          Return a relation that is the composition of the given relation and this relation.
 JMLValueToEqualsRelation difference(JMLValueToEqualsRelation othRel)
          Return a relation that is the difference between this and the given relation.
 JMLValueSet domain()
          Returns a set containing the domain of this relation.
 JMLValueSetEnumerator domainElements()
          Return a enumerator for the set that is the domain of this relation.
 JMLEqualsSet elementImage(JMLType dv)
          Returns a set containing all the range elements that this relation relates to the given domain element.
 JMLValueToEqualsRelationEnumerator elements()
          Return a enumerator for the set of associations that conceptually make up this relation.
 boolean equals(Object obj)
          Test whether this object's value is equal to the given argument.
 boolean has(Object obj)
          Tells whether this associates the given key to the given value.
 boolean has(JMLType dv, Object rv)
          Tells whether this associates the given key to the given value.
 boolean has(JMLValueEqualsPair pair)
          Tells whether this associates the given key to the given value.
 int hashCode()
          Return a hash code for this object.
 JMLEqualsSet 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.
 JMLValueToEqualsRelationImageEnumerator imagePairs()
          Return the set of domain image set pairs that make up this relation.
 JMLValueSet imagePairSet()
          Return the set of image set pairs that make up this relation.
 JMLValueToEqualsRelation insert(JMLValueEqualsPair pair)
          Return a relation that is just like this relation, except that it also includes the association described by the given pair.
 int int_size()
          Return the number of associations in this relation.
 JMLValueToEqualsRelation intersection(JMLValueToEqualsRelation othRel)
          Return a relation that is the intersection of this and the given relation.
 JMLEqualsToValueRelation inverse()
          Returns the inverse of this relation.
 JMLValueSet inverseElementImage(Object rv)
          Return a set of all the domain elements that relate to the given range element.
 JMLValueSet inverseImage(JMLEqualsSet rng)
          Return a set of all the domain elements that relate to some element in the given set of range elements.
 boolean isaFunction()
          Tells whether this relation is a function.
 boolean isDefinedAt(JMLType dv)
          Tells whether this relation associates any range element to the given domain element.
 boolean isEmpty()
          Tells whether the relation is empty.
 JMLIterator iterator()
          Returns an Iterator over the set of pairs conceptually contained in this relation..
 JMLEqualsSet range()
          Returns a set containing the range of this relation.
 JMLEqualsSetEnumerator rangeElements()
          Return a enumerator for the set that is the range of this relation.
 JMLValueToEqualsRelation remove(JMLType dv, Object 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.
 JMLValueToEqualsRelation remove(JMLValueEqualsPair pair)
          Return a relation that is just like this relation, except that it does not contain association described by the given pair.
 JMLValueToEqualsRelation 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.
 JMLValueToEqualsRelation 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.
 JMLValueToEqualsRelation restrictRangeTo(JMLEqualsSet rng)
          Return a relation that is like this relation except that its range is limited to just the elements of the given set.
static JMLValueToEqualsRelation singleton(JMLType dv, Object rv)
          Return the singleton relation containing the given association.
static JMLValueToEqualsRelation singleton(JMLValueEqualsPair pair)
          Return the singleton relation containing the association described by the given pair.
 JMLValueBag toBag()
          Return the bag of all associations in this relation.
 JMLValueToEqualsMap toFunction()
          Return a map that is contained in this relation.
 JMLValueSequence toSequence()
          Return a sequence containing all associations in this relation.
 JMLValueSet toSet()
          Return the set of all associations in this relation.
 String toString()
          Return a string representation of this object.
 JMLValueToEqualsRelation union(JMLValueToEqualsRelation othRel)
          Return a relation that union of the this and the given relation.
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 

Field Detail

domain_

protected final JMLValueSet domain_
The set of pairs of keys and values conceptually contained in this object. The set of elements in the domain of this relation.


imagePairSet_

protected final JMLValueSet imagePairSet_
The set representing the image pairs in the relation. The elements of this set are JMLValueValuePairs, which are all non-null. Each such pair has a key which is an element in domain_ and a value which is a JMLEqualsSet containing all of the elements that the key of the pair is related to.


size_

protected final int size_
The size (number of pairs) of this relation.


EMPTY

public static final JMLValueToEqualsRelation EMPTY
The empty JMLValueToEqualsRelation.

See Also:
JMLValueToEqualsRelation()

TOO_BIG_TO_INSERT

private static final String TOO_BIG_TO_INSERT

TOO_BIG_TO_UNION

protected static final String TOO_BIG_TO_UNION
Constructor Detail

JMLValueToEqualsRelation

public JMLValueToEqualsRelation()
Initialize this to be an empty relation. That is, the value is an empty set of pairs.

See Also:
EMPTY

JMLValueToEqualsRelation

public JMLValueToEqualsRelation(JMLType dv,
                                Object rv)
Initialize this to be a relation containing a single association between the given domain and range elements.

See Also:
singleton(JMLType, Object), JMLValueToEqualsRelation(JMLValueEqualsPair)

JMLValueToEqualsRelation

public JMLValueToEqualsRelation(JMLValueEqualsPair pair)
Initialize this to be a relation containing a single association given by the pair.

See Also:
singleton(JMLValueEqualsPair), JMLValueToEqualsRelation(JMLType, Object)

JMLValueToEqualsRelation

protected JMLValueToEqualsRelation(JMLValueSet ipset,
                                   JMLValueSet dom,
                                   int sz)
Initialize this using the given representation.

Method Detail

singleton

public static JMLValueToEqualsRelation singleton(JMLType dv,
                                                 Object rv)
Return the singleton relation containing the given association.

See Also:
singleton(JMLValueEqualsPair), JMLValueToEqualsRelation(JMLType, Object)

singleton

public static JMLValueToEqualsRelation singleton(JMLValueEqualsPair pair)
Return the singleton relation containing the association described by the given pair.

See Also:
singleton(JMLType, Object), JMLValueToEqualsRelation(JMLValueEqualsPair)

isaFunction

public boolean isaFunction()
Tells whether this relation is a function.

See Also:
JMLValueToEqualsMap

elementImage

public JMLEqualsSet elementImage(JMLType dv)
Returns a set containing all the range elements that this relation relates to the given domain element.

See Also:
image(org.jmlspecs.models.JMLValueSet), JMLValueToEqualsMap.apply(org.jmlspecs.models.JMLType)

image

public JMLEqualsSet 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.

See Also:
elementImage(org.jmlspecs.models.JMLType), inverseImage(org.jmlspecs.models.JMLEqualsSet), JMLValueToEqualsMap.apply(org.jmlspecs.models.JMLType)

inverse

public JMLEqualsToValueRelation inverse()
Returns the inverse of this relation. The inverse is the relation that relates each range element to the corresponding domain element.

See Also:
inverseImage(org.jmlspecs.models.JMLEqualsSet), inverseElementImage(java.lang.Object)

inverseElementImage

public JMLValueSet inverseElementImage(Object rv)
Return a set of all the domain elements that relate to the given range element.

See Also:
inverseImage(org.jmlspecs.models.JMLEqualsSet), inverse(), elementImage(org.jmlspecs.models.JMLType)

inverseImage

public JMLValueSet inverseImage(JMLEqualsSet rng)
Return a set of all the domain elements that relate to some element in the given set of range elements.

See Also:
inverseElementImage(java.lang.Object), inverse(), image(org.jmlspecs.models.JMLValueSet)

isDefinedAt

public boolean isDefinedAt(JMLType dv)
Tells whether this relation associates any range element to the given domain element.

See Also:
domain()

has

public boolean has(JMLType dv,
                   Object rv)
Tells whether this associates the given key to the given value.

See Also:
isDefinedAt(org.jmlspecs.models.JMLType), has(JMLValueEqualsPair)

has

public boolean has(JMLValueEqualsPair pair)
Tells whether this associates the given key to the given value.

See Also:
isDefinedAt(org.jmlspecs.models.JMLType), has(JMLType, Object)

has

public boolean has(Object obj)
Tells whether this associates the given key to the given value.

Specified by:
has in interface JMLCollection
See Also:
isDefinedAt(org.jmlspecs.models.JMLType), has(JMLValueEqualsPair)

isEmpty

public boolean isEmpty()
Tells whether the relation is empty.

See Also:
int_size()

clone

public Object clone()
Return a clone of this object.

Specified by:
clone in interface JMLType
Overrides:
clone in class Object

equals

public boolean equals(Object obj)
Test whether this object's value is equal to the given argument.

Specified by:
equals in interface JMLType
Overrides:
equals in class Object

hashCode

public int hashCode()
Return a hash code for this object.

Specified by:
hashCode in interface JMLType
Overrides:
hashCode in class Object

domain

public JMLValueSet domain()
Returns a set containing the domain of this relation.

See Also:
domainElements(), associations(), isDefinedAt(org.jmlspecs.models.JMLType), image(org.jmlspecs.models.JMLValueSet), range(), inverse()

range

public JMLEqualsSet range()
Returns a set containing the range of this relation.

See Also:
rangeElements(), associations(), inverseElementImage(java.lang.Object), domain(), inverse()

add

public JMLValueToEqualsRelation add(JMLType dv,
                                    Object rv)
                             throws NullPointerException,
                                    IllegalStateException
Return a relation that is just like this relation, except that it also associates the given domain element to the given range element.

Throws:
NullPointerException
IllegalStateException
See Also:
insert(org.jmlspecs.models.JMLValueEqualsPair)

insert

public JMLValueToEqualsRelation insert(JMLValueEqualsPair pair)
                                throws IllegalStateException
Return a relation that is just like this relation, except that it also includes the association described by the given pair.

Throws:
IllegalStateException
See Also:
add(org.jmlspecs.models.JMLType, java.lang.Object)

removeFromDomain

public JMLValueToEqualsRelation 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.

See Also:
remove(JMLValueEqualsPair), removeFromDomain(org.jmlspecs.models.JMLType)

remove

public JMLValueToEqualsRelation remove(JMLType dv,
                                       Object 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.

See Also:
removeFromDomain(org.jmlspecs.models.JMLType), remove(JMLType, Object), remove(JMLValueEqualsPair)

remove

public JMLValueToEqualsRelation remove(JMLValueEqualsPair pair)
Return a relation that is just like this relation, except that it does not contain association described by the given pair.

See Also:
remove(JMLType, Object), removeFromDomain(org.jmlspecs.models.JMLType)

compose

public JMLValueToEqualsRelation compose(JMLValueToValueRelation othRel)
Return a relation that is the composition of the given relation and this relation. The composition is done in the "usual" order, so that if the given relation relates x to y, and this relation relates y to z, then the result relates x to z.

See Also:
compose(JMLObjectToValueRelation)

compose

public JMLObjectToEqualsRelation compose(JMLObjectToValueRelation othRel)
Return a relation that is the composition of the given relation and this relation. The composition is done in the "usual" order, so that if the given relation relates x to y, and this relation relates y to z, then the result relates x to z.

See Also:
compose(JMLValueToValueRelation)

union

public JMLValueToEqualsRelation union(JMLValueToEqualsRelation othRel)
                               throws IllegalStateException
Return a relation that union of the this and the given relation. This is the union of the sets of associations.

Throws:
IllegalStateException
See Also:
difference(org.jmlspecs.models.JMLValueToEqualsRelation), intersection(org.jmlspecs.models.JMLValueToEqualsRelation)

intersection

public JMLValueToEqualsRelation intersection(JMLValueToEqualsRelation othRel)
Return a relation that is the intersection of this and the given relation. This is the intersection of the sets of associations.

See Also:
difference(org.jmlspecs.models.JMLValueToEqualsRelation), union(org.jmlspecs.models.JMLValueToEqualsRelation)

difference

public JMLValueToEqualsRelation difference(JMLValueToEqualsRelation othRel)
Return a relation that is the difference between this and the given relation. This is the difference between the sets of associations.

See Also:
difference(org.jmlspecs.models.JMLValueToEqualsRelation), intersection(org.jmlspecs.models.JMLValueToEqualsRelation)

restrictDomainTo

public JMLValueToEqualsRelation 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.

See Also:
restrictRangeTo(org.jmlspecs.models.JMLEqualsSet)

restrictRangeTo

public JMLValueToEqualsRelation restrictRangeTo(JMLEqualsSet rng)
Return a relation that is like this relation except that its range is limited to just the elements of the given set.

See Also:
restrictDomainTo(org.jmlspecs.models.JMLValueSet)

toString

public String toString()
Return a string representation of this object.

Overrides:
toString in class Object

associations

public JMLValueToEqualsRelationEnumerator associations()
Return a enumerator for the set of associations that conceptually make up this relation.

See Also:
elements(), iterator(), toSet(), imagePairs()

elements

public JMLValueToEqualsRelationEnumerator elements()
Return a enumerator for the set of associations that conceptually make up this relation. This is a synonym for associations.

See Also:
associations(), iterator()

iterator

public JMLIterator iterator()
Returns an Iterator over the set of pairs conceptually contained in this relation..

Specified by:
iterator in interface JMLCollection
See Also:
associations(), elements()

toSet

public JMLValueSet toSet()
Return the set of all associations in this relation.

See Also:
associations(), toBag(), toSequence()

toBag

public JMLValueBag toBag()
Return the bag of all associations in this relation.

See Also:
toSet(), toSequence()

toSequence

public JMLValueSequence toSequence()
Return a sequence containing all associations in this relation.

See Also:
toSet(), toBag()

imagePairSet

public JMLValueSet imagePairSet()
Return the set of image set pairs that make up this relation.

See Also:
imagePairs(), toSet()

imagePairs

public JMLValueToEqualsRelationImageEnumerator imagePairs()
Return the set of domain image set pairs that make up this relation.

See Also:
imagePairSet(), associations(), toSet()

domainElements

public JMLValueSetEnumerator domainElements()
Return a enumerator for the set that is the domain of this relation.

See Also:
domain(), rangeElements()

rangeElements

public JMLEqualsSetEnumerator rangeElements()
Return a enumerator for the set that is the range of this relation. (This was formerly called "elements").

See Also:
range(), domainElements()

int_size

public int int_size()
Return the number of associations in this relation.

Specified by:
int_size in interface JMLCollection

toFunction

public JMLValueToEqualsMap toFunction()
Return a map that is contained in this relation. If this relation is a function, then this method can be seen as a type conversion which does not make a change to the abstract value. However, if this relation is not a function, then this method chooses a function contained in this relation from among the possibilities available.

See Also:
isaFunction(), JMLValueToEqualsMap

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.