JML

org.jmlspecs.models
Class JMLObjectToObjectRelation

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

public class JMLObjectToObjectRelation
extends Object
implements JMLCollection

Binary relations (or set-valued functions) from non-null elements of Object to non-null elements of Object. The first type, Object, 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 JMLObjectSet).

This type considers elements val and dv of the domain type, to be distinct just when val != dv. It considers elements of r and rv of the range type to be distinct just when r != 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, JMLObjectToObjectMap, JMLObjectToObjectRelationEnumerator, JMLObjectToObjectRelationImageEnumerator, JMLValueSet, JMLObjectSet, JMLObjectToObjectRelation, JMLValueToObjectRelation, JMLObjectToValueRelation, JMLValueToValueRelation

Class Specifications
public invariant ( \forall java.lang.Object obj; this.theRelation.has((org.jmlspecs.models.JMLType)obj); obj != null&&obj instanceof org.jmlspecs.models.JMLObjectObjectPair&&((org.jmlspecs.models.JMLObjectObjectPair)obj).key != null&&((org.jmlspecs.models.JMLObjectObjectPair)obj).value != null);
public invariant_redundantly (* Every element of 'theRelation'is a JMLObjectObjectPair whose key and value are not null *);
public invariant this.elementType == \type(org.jmlspecs.models.JMLObjectObjectPair);
public invariant !this.containsNull;
protected invariant this.imagePairSet_.int_size() == this.domain_.int_size()&&( \forall java.lang.Object dv; dv != null&&this.domain_.has(dv); this.imagePairSet_.has(new org.jmlspecs.models.JMLObjectValuePair(dv, this.elementImage(dv))));
protected invariant_redundantly this.imagePairSet_ == this.imagePairSet();
protected invariant this.size_ == this.theRelation.int_size();
protected invariant this.size_ >= 0;
public invariant this.owner == null;
protected represents theRelation <- this.toSet();

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Specifications inherited from interface JMLCollection
instance public constraint this.elementType == \old(this.elementType);
instance public constraint this.containsNull == \old(this.containsNull);

Model Field Summary
 JMLValueSet theRelation
          The set of pairs of keys and values conceptually contained in this object.
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Model fields inherited from interface org.jmlspecs.models.JMLCollection
elementState
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Ghost fields inherited from interface org.jmlspecs.models.JMLCollection
containsNull, elementType
 
Field Summary
protected  JMLObjectSet domain_
          The set of elements in the domain of this relation.
static JMLObjectToObjectRelation EMPTY
          The empty JMLObjectToObjectRelation.
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
  JMLObjectToObjectRelation()
          Initialize this to be an empty relation.
  JMLObjectToObjectRelation(non_null Object dv, non_null Object rv)
          Initialize this to be a relation containing a single association between the given domain and range elements.
  JMLObjectToObjectRelation(non_null JMLObjectObjectPair pair)
          Initialize this to be a relation containing a single association given by the pair.
protected JMLObjectToObjectRelation(non_null JMLValueSet ipset, non_null JMLObjectSet dom, int sz)
          Initialize this using the given representation.
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Model methods inherited from interface org.jmlspecs.models.JMLCollection
size
 
Method Summary
 JMLObjectToObjectRelation add(non_null Object dv, non_null 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.
 JMLObjectToObjectRelationEnumerator associations()
          Return a enumerator for the set of associations that conceptually make up this relation.
 Object clone()
          Return a clone of this object.
 JMLObjectToObjectRelation compose(non_null JMLObjectToObjectRelation othRel)
          Return a relation that is the composition of the given relation and this relation.
 JMLValueToObjectRelation compose(non_null JMLValueToObjectRelation othRel)
          Return a relation that is the composition of the given relation and this relation.
 JMLObjectToObjectRelation difference(non_null JMLObjectToObjectRelation othRel)
          Return a relation that is the difference between this and the given relation.
 JMLObjectSet domain()
          Returns a set containing the domain of this relation.
 JMLObjectSetEnumerator domainElements()
          Return a enumerator for the set that is the domain of this relation.
 JMLObjectSet elementImage(nullable Object dv)
          Returns a set containing all the range elements that this relation relates to the given domain element.
 JMLObjectToObjectRelationEnumerator elements()
          Return a enumerator for the set of associations that conceptually make up this relation.
 boolean equals(nullable Object obj)
          Test whether this object's value is equal to the given argument.
 boolean has(nullable Object obj)
          Tells whether this associates the given key to the given value.
 boolean has(nullable Object dv, nullable Object rv)
          Tells whether this associates the given key to the given value.
 boolean has(non_null JMLObjectObjectPair pair)
          Tells whether this associates the given key to the given value.
 int hashCode()
          Return a hash code for this object.
 JMLObjectSet image(non_null JMLObjectSet dom)
          Returns a set containing all the range elements that this relation relates to the elements of the given set of domain elements.
 JMLObjectToObjectRelationImageEnumerator 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.
 JMLObjectToObjectRelation insert(non_null JMLObjectObjectPair 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.
 JMLObjectToObjectRelation intersection(non_null JMLObjectToObjectRelation othRel)
          Return a relation that is the intersection of this and the given relation.
 JMLObjectToObjectRelation inverse()
          Returns the inverse of this relation.
 JMLObjectSet inverseElementImage(Object rv)
          Return a set of all the domain elements that relate to the given range element.
 JMLObjectSet inverseImage(non_null JMLObjectSet 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(Object 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..
 JMLObjectSet range()
          Returns a set containing the range of this relation.
 JMLObjectSetEnumerator rangeElements()
          Return a enumerator for the set that is the range of this relation.
 JMLObjectToObjectRelation remove(Object 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.
 JMLObjectToObjectRelation remove(non_null JMLObjectObjectPair pair)
          Return a relation that is just like this relation, except that it does not contain association described by the given pair.
 JMLObjectToObjectRelation removeFromDomain(nullable Object dv)
          Return a relation that is just like this relation, except that it does not contain any association with the given domain element.
 JMLObjectToObjectRelation restrictDomainTo(non_null JMLObjectSet dom)
          Return a relation that is like this relation except that its domain is limited to just the elements of the given set.
 JMLObjectToObjectRelation restrictRangeTo(non_null JMLObjectSet rng)
          Return a relation that is like this relation except that its range is limited to just the elements of the given set.
static JMLObjectToObjectRelation singleton(non_null Object dv, non_null Object rv)
          Return the singleton relation containing the given association.
static JMLObjectToObjectRelation singleton(non_null JMLObjectObjectPair pair)
          Return the singleton relation containing the association described by the given pair.
 JMLValueBag toBag()
          Return the bag of all associations in this relation.
 JMLObjectToObjectMap 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.
 JMLObjectToObjectRelation union(non_null JMLObjectToObjectRelation 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
 

Model Field Detail

theRelation

public JMLValueSet theRelation
The set of pairs of keys and values conceptually contained in this object.

Specifications:
datagroup contains: domain_ imagePairSet_ size_
Field Detail

domain_

protected final JMLObjectSet domain_
The set of elements in the domain of this relation.

Specifications: non_null
is in groups: theRelation

imagePairSet_

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

Specifications: non_null
is in groups: theRelation

size_

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

Specifications:
is in groups: theRelation

EMPTY

public static final JMLObjectToObjectRelation EMPTY
The empty JMLObjectToObjectRelation.

See Also:
JMLObjectToObjectRelation()
Specifications: non_null

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

JMLObjectToObjectRelation

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

See Also:
EMPTY
Specifications: (class)pure
public normal_behavior
assignable theRelation, owner, elementType, containsNull;
ensures this.theRelation.equals(new org.jmlspecs.models.JMLValueSet());
ensures_redundantly this.theRelation.isEmpty();

JMLObjectToObjectRelation

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

See Also:
singleton(Object, Object), JMLObjectToObjectRelation(JMLObjectObjectPair)
Specifications: (class)pure
public normal_behavior
requires dv != null&&rv != null;
assignable theRelation, owner, elementType, containsNull;
ensures this.theRelation.int_size() == 1;
ensures this.elementImage(dv).has(rv);
ensures_redundantly this.isDefinedAt(dv);

JMLObjectToObjectRelation

public JMLObjectToObjectRelation(non_null JMLObjectObjectPair pair)
Initialize this to be a relation containing a single association given by the pair.

See Also:
singleton(JMLObjectObjectPair), JMLObjectToObjectRelation(Object, Object)
Specifications: (class)pure
public normal_behavior
requires pair != null;
assignable theRelation, owner, elementType, containsNull;
ensures this.theRelation.int_size() == 1&&this.theRelation.has(pair);

JMLObjectToObjectRelation

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

Specifications: (class)pure
protected normal_behavior
requires ipset != null&&dom != null&&dom.int_size() <= sz;
assignable theRelation, owner, elementType, containsNull;
assignable_redundantly domain_, imagePairSet_, size_;
ensures this.imagePairSet_ == ipset&&this.domain_ == dom&&this.size_ == sz;
    implies_that
requires ipset != null&&dom != null&&0 <= sz;
ensures this.imagePairSet_ == ipset&&this.domain_ == dom&&this.size_ == sz;
Method Detail

singleton

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

See Also:
singleton(JMLObjectObjectPair), JMLObjectToObjectRelation(Object, Object)
Specifications: pure non_null
public normal_behavior
requires dv != null&&rv != null;
ensures \result != null&&\result .equals(new org.jmlspecs.models.JMLObjectToObjectRelation(dv, rv));

singleton

public static JMLObjectToObjectRelation singleton(non_null JMLObjectObjectPair pair)
Return the singleton relation containing the association described by the given pair.

See Also:
singleton(Object, Object), JMLObjectToObjectRelation(JMLObjectObjectPair)
Specifications: pure non_null
public normal_behavior
requires pair != null;
ensures \result != null&&\result .equals(singleton(pair.key,pair.value));

isaFunction

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

See Also:
JMLObjectToObjectMap
Specifications: (class)pure
public normal_behavior
ensures \result == ( \forall java.lang.Object dv; this.isDefinedAt(dv); this.elementImage(dv).int_size() == 1);

elementImage

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

See Also:
image(org.jmlspecs.models.JMLObjectSet), JMLObjectToObjectMap.apply(java.lang.Object)
Specifications: non_null (class)pure
public normal_behavior
ensures ( \forall org.jmlspecs.models.JMLObjectObjectPair pair; this.theRelation.has(pair); pair.keyEquals(dv) ==> \result .has(pair.value));
ensures ( \forall java.lang.Object o; \result .has(o); ( \exists org.jmlspecs.models.JMLObjectObjectPair pair; this.theRelation.has(pair); pair.keyEquals(dv)&&pair.valueEquals(o)));
ensures_redundantly !this.isDefinedAt(dv) ==> \result .isEmpty();
    implies_that
ensures \result != null&&!\result .containsNull;

image

public JMLObjectSet image(non_null JMLObjectSet 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(java.lang.Object), inverseImage(org.jmlspecs.models.JMLObjectSet), JMLObjectToObjectMap.apply(java.lang.Object)
Specifications: non_null (class)pure
public normal_behavior
requires dom != null;
ensures ( \forall java.lang.Object o; ; \result .has(o) <==> ( \exists org.jmlspecs.models.JMLObjectObjectPair pair; this.theRelation.has(pair); dom.has(pair.key)&&pair.valueEquals(o)));
ensures_redundantly ( \forall org.jmlspecs.models.JMLObjectObjectPair pair; this.theRelation.has(pair); dom.has(pair.key) ==> \result .has(pair.value));
    implies_that
ensures \result != null&&!\result .containsNull;

inverse

public JMLObjectToObjectRelation 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.JMLObjectSet), inverseElementImage(java.lang.Object)
Specifications: non_null (class)pure
public normal_behavior
ensures ( \forall org.jmlspecs.models.JMLObjectObjectPair pair; ; \result .theRelation.has(pair) == this.elementImage(pair.value).has(pair.key));

inverseElementImage

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

See Also:
inverseImage(org.jmlspecs.models.JMLObjectSet), inverse(), elementImage(java.lang.Object)
Specifications: non_null (class)pure
public normal_behavior
ensures \result .equals(this.inverse().elementImage(rv));
    implies_that
ensures \result != null&&!\result .containsNull;

inverseImage

public JMLObjectSet inverseImage(non_null JMLObjectSet 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.JMLObjectSet)
Specifications: non_null (class)pure
public normal_behavior
requires rng != null;
ensures \result .equals(this.inverse().image(rng));
    implies_that
ensures \result != null&&!\result .containsNull;

isDefinedAt

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

See Also:
domain()
Specifications: (class)pure
public normal_behavior
ensures \result == (this.elementImage(dv).int_size() > 0);
ensures_redundantly dv == null ==> !\result ;

has

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

See Also:
isDefinedAt(java.lang.Object), has(JMLObjectObjectPair)
Specifications: pure
public normal_behavior
ensures \result <==> this.domain().has(dv)&&this.elementImage(dv).has(rv);
ensures_redundantly dv == null||rv == null ==> !\result ;

has

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

See Also:
isDefinedAt(java.lang.Object), has(Object, Object)
Specifications: pure
public normal_behavior
requires pair != null;
ensures \result <==> this.has(pair.key,pair.value);
Specifications inherited from overridden method has(Object elem) in interface JMLCollection:
       pure
public normal_behavior
ensures (* \result <==> elem is equal to one of the elements in the collection. *);
ensures_redundantly !this.containsNull&&elem == null ==> !\result ;
ensures_redundantly elem != null&&!(\typeof(elem) <: this.elementType) ==> !\result ;

has

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

Specified by:
has in interface JMLCollection
See Also:
isDefinedAt(java.lang.Object), has(JMLObjectObjectPair)
Specifications: pure
     also
public normal_behavior
ensures \result <==> obj != null&&obj instanceof org.jmlspecs.models.JMLObjectObjectPair&&this.has((org.jmlspecs.models.JMLObjectObjectPair)obj);
Specifications inherited from overridden method has(Object elem) in interface JMLCollection:
       pure
public normal_behavior
ensures (* \result <==> elem is equal to one of the elements in the collection. *);
ensures_redundantly !this.containsNull&&elem == null ==> !\result ;
ensures_redundantly elem != null&&!(\typeof(elem) <: this.elementType) ==> !\result ;

isEmpty

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

See Also:
int_size()
Specifications: (class)pure
public normal_behavior
ensures \result == (this.theRelation.int_size() == 0);

clone

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

Specified by:
clone in interface JMLType
Overrides:
clone in class Object
Specifications: (class)pure
     also
public normal_behavior
ensures \result instanceof org.jmlspecs.models.JMLObjectToObjectRelation&&((org.jmlspecs.models.JMLObjectToObjectRelation)\result ).theRelation.equals(this.theRelation);
Specifications inherited from overridden method in class Object:
       non_null
protected normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures \result != null;
ensures \typeof(\result ) == \typeof(this);
ensures (* \result is a clone of this *);
     also
protected normal_behavior
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);
     also
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures java.lang.reflect.Array.getLength(\result ) == java.lang.reflect.Array.getLength(this);
ensures ( \forall int i; 0 <= i&&i < java.lang.reflect.Array.getLength(this); ( \exists java.lang.Object result_i; result_i == java.lang.reflect.Array.get(\result ,i); (result_i == null&&java.lang.reflect.Array.get(this,i) == null)||(result_i != null&&result_i.equals(java.lang.reflect.Array.get(this,i)))));
     also
protected exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
assignable \nothing;
signals_only java.lang.CloneNotSupportedException;
     also
protected normal_behavior
requires \elemtype(\typeof(this)) <: \type(java.lang.Object);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(int);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((int[])\result ).length == ((int[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((int[])this).length; ((int[])\result )[i] == ((int[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(byte);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((byte[])\result ).length == ((byte[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((byte[])this).length; ((byte[])\result )[i] == ((byte[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(char);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((char[])\result ).length == ((char[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((char[])this).length; ((char[])\result )[i] == ((char[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(long);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((long[])\result ).length == ((long[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((long[])this).length; ((long[])\result )[i] == ((long[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(short);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((short[])\result ).length == ((short[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((short[])this).length; ((short[])\result )[i] == ((short[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(boolean);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((boolean[])\result ).length == ((boolean[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((boolean[])this).length; ((boolean[])\result )[i] == ((boolean[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(float);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((float[])\result ).length == ((float[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((float[])this).length; (java.lang.Float.isNaN(((float[])\result )[i])&&java.lang.Float.isNaN(((float[])this)[i]))||((float[])\result )[i] == ((float[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(double);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((double[])\result ).length == ((double[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((double[])this).length; (java.lang.Double.isNaN(((double[])\result )[i])&&java.lang.Double.isNaN(((double[])this)[i]))||((double[])\result )[i] == ((double[])this)[i]);
Specifications inherited from overridden method in interface JMLType:
       pure
     also
public normal_behavior
ensures \result != null;
ensures \result instanceof org.jmlspecs.models.JMLType;
ensures ((org.jmlspecs.models.JMLType)\result ).equals(this);
    implies_that
ensures \result != null&&\typeof(\result ) <: \type(org.jmlspecs.models.JMLType);

equals

public boolean equals(nullable 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
Specifications: (class)pure
     also
public normal_behavior
requires obj != null&&obj instanceof org.jmlspecs.models.JMLObjectToObjectRelation;
ensures \result == this.theRelation.equals(((org.jmlspecs.models.JMLObjectToObjectRelation)obj).theRelation);
     also
public normal_behavior
requires obj == null||!(obj instanceof org.jmlspecs.models.JMLObjectToObjectRelation);
ensures !\result ;
Specifications inherited from overridden method equals(Object obj) in class Object:
       pure
public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);
     also
public normal_behavior
requires this == obj;
ensures \result ;
     also
public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;
     also
diverges false;
ensures obj == null ==> !\result ;
Specifications inherited from overridden method equals(Object ob2) in interface JMLType:
       pure
     also
public normal_behavior
ensures \result ==> ob2 != null&&(* ob2 is not distinguishable from this, except by using mutation or == *);
    implies_that
public normal_behavior
{|
requires ob2 != null&&ob2 instanceof org.jmlspecs.models.JMLType;
ensures ((org.jmlspecs.models.JMLType)ob2).equals(this) == \result ;
also
requires ob2 == this;
ensures \result <==> true;
|}

hashCode

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

Specified by:
hashCode in interface JMLType
Overrides:
hashCode in class Object
Specifications: (class)pure
Specifications inherited from overridden method in class Object:
public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);
     also
public code normal_behavior
assignable \nothing;
Specifications inherited from overridden method in interface JMLType:
       pure

domain

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

See Also:
domainElements(), associations(), isDefinedAt(java.lang.Object), image(org.jmlspecs.models.JMLObjectSet), range(), inverse()
Specifications: non_null (class)pure
public normal_behavior
ensures ( \forall java.lang.Object dv; ; \result .has(dv) == this.isDefinedAt(dv));

range

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

See Also:
rangeElements(), associations(), inverseElementImage(java.lang.Object), domain(), inverse()
Specifications: non_null (class)pure
public normal_behavior
ensures ( \forall java.lang.Object rv; ; \result .has(rv) == ( \exists java.lang.Object dv; ; this.elementImage(dv).has(rv)));

add

public JMLObjectToObjectRelation add(non_null Object dv,
                                     non_null 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.JMLObjectObjectPair)
Specifications: pure non_null
public normal_behavior
requires dv != null&&rv != null;
requires this.int_size() < 2147483647||this.elementImage(dv).has(rv);
ensures \result .theRelation.equals(this.theRelation.insert(new org.jmlspecs.models.JMLObjectObjectPair(dv, rv)));

insert

public JMLObjectToObjectRelation insert(non_null JMLObjectObjectPair 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(java.lang.Object, java.lang.Object)
Specifications: non_null (class)pure
public normal_behavior
requires pair != null;
requires this.int_size() < 2147483647||this.elementImage(pair.key).has(pair.value);
ensures \result .theRelation.equals(this.theRelation.insert(pair));

removeFromDomain

public JMLObjectToObjectRelation removeFromDomain(nullable Object 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(JMLObjectObjectPair), removeFromDomain(java.lang.Object)
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&( \forall java.lang.Object val; this.domain().has(val); ( \forall java.lang.Object r; r != null; (this.elementImage(val).has(r) <==> \result .theRelation.has(new org.jmlspecs.models.JMLObjectObjectPair(val, r))&&val != dv)));
    implies_that
public normal_behavior
requires dv == null;
ensures \result != null&&\result .equals(this);

remove

public JMLObjectToObjectRelation remove(Object 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(java.lang.Object), remove(Object, Object), remove(JMLObjectObjectPair)
Specifications: non_null (class)pure
public normal_behavior
requires dv != null&&rv != null;
ensures \result .theRelation.equals(this.theRelation.remove(new org.jmlspecs.models.JMLObjectObjectPair(dv, rv)));
     also
requires dv == null||rv == null;
ensures \result != null&&\result .equals(this);

remove

public JMLObjectToObjectRelation remove(non_null JMLObjectObjectPair 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(Object, Object), removeFromDomain(java.lang.Object)
Specifications: non_null (class)pure
public normal_behavior
requires pair != null;
ensures \result .theRelation.equals(this.theRelation.remove(pair));

compose

public JMLValueToObjectRelation compose(non_null JMLValueToObjectRelation 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(JMLObjectToObjectRelation)
Specifications: non_null (class)pure
public normal_behavior
requires othRel != null;
ensures ( \forall org.jmlspecs.models.JMLValueObjectPair pair; ; \result .theRelation.has(pair) == ( \exists java.lang.Object val; othRel.elementImage(pair.key).has(val); this.elementImage(val).has(pair.value)));

compose

public JMLObjectToObjectRelation compose(non_null JMLObjectToObjectRelation 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(JMLValueToObjectRelation)
Specifications: non_null (class)pure
public normal_behavior
requires othRel != null;
ensures ( \forall org.jmlspecs.models.JMLValueObjectPair pair; ; \result .theRelation.has(pair) == ( \exists java.lang.Object val; othRel.elementImage(pair.key).has(val); this.elementImage(val).has(pair.value)));

union

public JMLObjectToObjectRelation union(non_null JMLObjectToObjectRelation 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.JMLObjectToObjectRelation), intersection(org.jmlspecs.models.JMLObjectToObjectRelation)
Specifications: non_null (class)pure
public normal_behavior
requires othRel != null;
requires this.int_size() < 2147483647-othRel.difference(this).int_size();
ensures \result .theRelation.equals(this.theRelation.union(othRel.theRelation));

intersection

public JMLObjectToObjectRelation intersection(non_null JMLObjectToObjectRelation 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.JMLObjectToObjectRelation), union(org.jmlspecs.models.JMLObjectToObjectRelation)
Specifications: non_null (class)pure
public normal_behavior
requires othRel != null;
ensures \result .theRelation.equals(this.theRelation.intersection(othRel.theRelation));

difference

public JMLObjectToObjectRelation difference(non_null JMLObjectToObjectRelation 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.JMLObjectToObjectRelation), intersection(org.jmlspecs.models.JMLObjectToObjectRelation)
Specifications: non_null (class)pure
public normal_behavior
requires othRel != null;
ensures \result .theRelation.equals(this.theRelation.difference(othRel.theRelation));

restrictDomainTo

public JMLObjectToObjectRelation restrictDomainTo(non_null JMLObjectSet 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.JMLObjectSet)
Specifications: non_null (class)pure
public normal_behavior
requires dom != null;
ensures ( \forall org.jmlspecs.models.JMLObjectObjectPair pair; pair != null; \result .theRelation.has(pair) == dom.has(pair.key)&&this.elementImage(pair.key).has(pair.value));

restrictRangeTo

public JMLObjectToObjectRelation restrictRangeTo(non_null JMLObjectSet 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.JMLObjectSet)
Specifications: non_null (class)pure
public normal_behavior
requires rng != null;
ensures ( \forall org.jmlspecs.models.JMLObjectObjectPair pair; ; \result .theRelation.has(pair) == rng.has(pair.value)&&this.elementImage(pair.key).has(pair.value));

toString

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

Overrides:
toString in class Object
Specifications: (class)pure
     also
public normal_behavior
ensures \result .equals(this.theRelation.toString());
Specifications inherited from overridden method in class Object:
       non_null
public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);
     also
public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);
     also
public code model_program { ... }
    implies_that
assignable objectState;
ensures \result != null;

associations

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

See Also:
elements(), iterator(), toSet(), imagePairs()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .equals(new org.jmlspecs.models.JMLObjectToObjectRelationEnumerator(this));

elements

public JMLObjectToObjectRelationEnumerator 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()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .equals(this.associations());

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()
Specifications: (class)pure
     also
public normal_behavior
ensures \fresh(\result )&&\result .equals(new org.jmlspecs.models.JMLEnumerationToIterator(this.elements()));
Specifications inherited from overridden method in interface JMLCollection:
       pure non_null
public normal_behavior
ensures \fresh(\result )&&\result .elementType == this.elementType;
ensures !this.containsNull ==> !\result .returnsNull;

toSet

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

See Also:
associations(), toBag(), toSequence()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .size == this.int_size()&&( \forall org.jmlspecs.models.JMLType pv; \result .has(pv); pv != null&&pv instanceof org.jmlspecs.models.JMLObjectObjectPair&&this.isDefinedAt(((org.jmlspecs.models.JMLObjectObjectPair)pv).key)&&this.elementImage(((org.jmlspecs.models.JMLObjectObjectPair)pv).key).has(((org.jmlspecs.models.JMLObjectObjectPair)pv).value));

toBag

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

See Also:
toSet(), toSequence()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .equals(this.toSet().toBag());

toSequence

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

See Also:
toSet(), toBag()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&( \forall org.jmlspecs.models.JMLObjectObjectPair p; ; \result .count(p) == 1 <==> this.has(p));

imagePairSet

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

See Also:
imagePairs(), toSet()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .int_size() == this.domain().int_size()&&( \forall java.lang.Object dv; this.domain().has(dv); \result .has(new org.jmlspecs.models.JMLObjectValuePair(dv, this.elementImage(dv))));

imagePairs

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

See Also:
imagePairSet(), associations(), toSet()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .abstractValue().int_size() == this.domain().int_size()&&( \forall java.lang.Object dv; this.domain().has(dv); \result .abstractValue().has(new org.jmlspecs.models.JMLObjectValuePair(dv, this.elementImage(dv))));

domainElements

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

See Also:
domain(), rangeElements()
Specifications: non_null (class)pure
public normal_behavior
ensures \result .equals(this.domain().elements());

rangeElements

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

See Also:
range(), domainElements()
Specifications: non_null (class)pure
public normal_behavior
ensures \result .equals(this.range().elements());

int_size

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

Specified by:
int_size in interface JMLCollection
Specifications: (class)pure
     also
public normal_behavior
ensures \result == this.theRelation.int_size();
Specifications inherited from overridden method in interface JMLCollection:
       pure
public normal_behavior
requires this.size() <= 2147483647;
ensures \result == this.size();

toFunction

public JMLObjectToObjectMap 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(), JMLObjectToObjectMap
Specifications: non_null (class)pure
public normal_behavior
ensures ( \forall java.lang.Object dv; dv != null; (this.isDefinedAt(dv) == \result .isDefinedAt(dv))&&\result .elementImage(dv).isSubset(this.elementImage(dv))&&\result .elementImage(dv).int_size() == 1);

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.