org.jmlspecs.models
Class JMLValueToValueRelation

java.lang.Object
  org.jmlspecs.models.JMLValueToValueRelation

All Implemented Interfaces:

Cloneable, JMLCollection, JMLType, Serializable

Direct Known Subclasses:

JMLValueToValueMap

public class JMLValueToValueRelation

extends Object

implements JMLCollection

Binary relations (or set-valued functions) from non-null elements of JMLType to non-null elements of JMLType. The first type, JMLType, is called the domain type of the relation; the second type, JMLType, 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 JMLValueSet).

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, JMLValueToValueMap, JMLValueToValueRelationEnumerator, JMLValueToValueRelationImageEnumerator, 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.JMLValueValuePair&&((org.jmlspecs.models.JMLValueValuePair)obj).key != null&&((org.jmlspecs.models.JMLValueValuePair)obj).value != null); public invariant_redundantly (* Every element of 'theRelation'is a JMLValueValuePair whose key and value are not null *); public invariant this.elementType == \type(org.jmlspecs.models.JMLValueValuePair); public invariant !this.containsNull; protected invariant this.imagePairSet_.int_size() == this.domain_.int_size()&&( \forall org.jmlspecs.models.JMLType dv; dv != null&&this.domain_.has(dv); this.imagePairSet_.has(new org.jmlspecs.models.JMLValueValuePair(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  JMLValueSet	domain_           The set of elements in the domain of this relation.
static JMLValueToValueRelation	EMPTY           The empty JMLValueToValueRelation.
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
	JMLValueToValueRelation()           Initialize this to be an empty relation.
	JMLValueToValueRelation(non_null JMLType dv, non_null JMLType rv)           Initialize this to be a relation containing a single association between the given domain and range elements.
protected	JMLValueToValueRelation(non_null JMLValueSet ipset, non_null JMLValueSet dom, int sz)           Initialize this using the given representation.
	JMLValueToValueRelation(non_null JMLValueValuePair pair)           Initialize this to be a relation containing a single association given by the pair.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface org.jmlspecs.models.JMLCollection

size

 

Method Summary
JMLValueToValueRelation	add(non_null JMLType dv, non_null 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.
JMLValueToValueRelationEnumerator	associations()           Return a enumerator for the set of associations that conceptually make up this relation.
Object	clone()           Return a clone of this object.
JMLObjectToValueRelation	compose(non_null JMLObjectToValueRelation othRel)           Return a relation that is the composition of the given relation and this relation.
JMLValueToValueRelation	compose(non_null JMLValueToValueRelation othRel)           Return a relation that is the composition of the given relation and this relation.
JMLValueToValueRelation	difference(non_null JMLValueToValueRelation 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.
JMLValueSet	elementImage(nullable JMLType dv)           Returns a set containing all the range elements that this relation relates to the given domain element.
JMLValueToValueRelationEnumerator	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 JMLType dv, nullable JMLType rv)           Tells whether this associates the given key to the given value.
boolean	has(non_null JMLValueValuePair pair)           Tells whether this associates the given key to the given value.
int	hashCode()           Return a hash code for this object.
JMLValueSet	image(non_null JMLValueSet dom)           Returns a set containing all the range elements that this relation relates to the elements of the given set of domain elements.
JMLValueToValueRelationImageEnumerator	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.
JMLValueToValueRelation	insert(non_null JMLValueValuePair 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.
JMLValueToValueRelation	intersection(non_null JMLValueToValueRelation othRel)           Return a relation that is the intersection of this and the given relation.
JMLValueToValueRelation	inverse()           Returns the inverse of this relation.
JMLValueSet	inverseElementImage(JMLType rv)           Return a set of all the domain elements that relate to the given range element.
JMLValueSet	inverseImage(non_null JMLValueSet 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..
JMLValueSet	range()           Returns a set containing the range of this relation.
JMLValueSetEnumerator	rangeElements()           Return a enumerator for the set that is the range of this relation.
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.
JMLValueToValueRelation	remove(non_null JMLValueValuePair pair)           Return a relation that is just like this relation, except that it does not contain association described by the given pair.
JMLValueToValueRelation	removeFromDomain(nullable JMLType dv)           Return a relation that is just like this relation, except that it does not contain any association with the given domain element.
JMLValueToValueRelation	restrictDomainTo(non_null JMLValueSet dom)           Return a relation that is like this relation except that its domain is limited to just the elements of the given set.
JMLValueToValueRelation	restrictRangeTo(non_null JMLValueSet rng)           Return a relation that is like this relation except that its range is limited to just the elements of the given set.
static JMLValueToValueRelation	singleton(non_null JMLType dv, non_null JMLType rv)           Return the singleton relation containing the given association.
static JMLValueToValueRelation	singleton(non_null JMLValueValuePair pair)           Return the singleton relation containing the association described by the given pair.
JMLValueBag	toBag()           Return the bag of all associations in this relation.
JMLValueToValueMap	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.
JMLValueToValueRelation	union(non_null JMLValueToValueRelation 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_

domain_

protected final JMLValueSet 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 JMLValueValuePairs, which are all non-null. Each such pair has a key which is an element in domain_ and a value which is a JMLValueSet 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 JMLValueToValueRelation EMPTY

The empty JMLValueToValueRelation.

See Also:

JMLValueToValueRelation()

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

JMLValueToValueRelation

public JMLValueToValueRelation()

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();

JMLValueToValueRelation

public JMLValueToValueRelation(non_null JMLType dv,
                               non_null JMLType rv)

Initialize this to be a relation containing a single association between the given domain and range elements.

See Also:

singleton(JMLType, JMLType), JMLValueToValueRelation(JMLValueValuePair)

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);

JMLValueToValueRelation

public JMLValueToValueRelation(non_null JMLValueValuePair pair)

Initialize this to be a relation containing a single association given by the pair.

See Also:

singleton(JMLValueValuePair), JMLValueToValueRelation(JMLType, JMLType)

Specifications: (class)pure

public normal_behavior
requires pair != null;
assignable theRelation, owner, elementType, containsNull;
ensures this.theRelation.int_size() == 1&&this.theRelation.has(pair);

JMLValueToValueRelation

protected JMLValueToValueRelation(non_null JMLValueSet ipset,
                                  non_null JMLValueSet 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;

singleton

public static JMLValueToValueRelation singleton(non_null JMLType dv,
                                                non_null JMLType rv)

Return the singleton relation containing the given association.

See Also:

singleton(JMLValueValuePair), JMLValueToValueRelation(JMLType, JMLType)

Specifications: pure non_null

public normal_behavior
requires dv != null&&rv != null;
ensures \result != null&&\result .equals(new org.jmlspecs.models.JMLValueToValueRelation(dv, rv));

singleton

public static JMLValueToValueRelation singleton(non_null JMLValueValuePair pair)

Return the singleton relation containing the association described by the given pair.

See Also:

singleton(JMLType, JMLType), JMLValueToValueRelation(JMLValueValuePair)

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:

JMLValueToValueMap

Specifications: (class)pure

public normal_behavior
ensures \result == ( \forall org.jmlspecs.models.JMLType dv; this.isDefinedAt(dv); this.elementImage(dv).int_size() == 1);

elementImage

public JMLValueSet elementImage(nullable 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), JMLValueToValueMap.apply(org.jmlspecs.models.JMLType)

Specifications: non_null (class)pure

public normal_behavior
ensures ( \forall org.jmlspecs.models.JMLValueValuePair pair; this.theRelation.has(pair); pair.keyEquals(dv) ==> \result .has(pair.value));
ensures ( \forall org.jmlspecs.models.JMLType o; \result .has(o); ( \exists org.jmlspecs.models.JMLValueValuePair 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 JMLValueSet image(non_null 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.JMLValueSet), JMLValueToValueMap.apply(org.jmlspecs.models.JMLType)

Specifications: non_null (class)pure

public normal_behavior
requires dom != null;
ensures ( \forall org.jmlspecs.models.JMLType o; ; \result .has(o) <==> ( \exists org.jmlspecs.models.JMLValueValuePair pair; this.theRelation.has(pair); dom.has(pair.key)&&pair.valueEquals(o)));
ensures_redundantly ( \forall org.jmlspecs.models.JMLValueValuePair pair; this.theRelation.has(pair); dom.has(pair.key) ==> \result .has(pair.value));

    implies_that

ensures \result != null&&!\result .containsNull;

inverse

public JMLValueToValueRelation 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.JMLValueSet), inverseElementImage(org.jmlspecs.models.JMLType)

Specifications: non_null (class)pure

public normal_behavior
ensures ( \forall org.jmlspecs.models.JMLValueValuePair pair; ; \result .theRelation.has(pair) == this.elementImage(pair.value).has(pair.key));

inverseElementImage

public JMLValueSet inverseElementImage(JMLType rv)

Return a set of all the domain elements that relate to the given range element.

See Also:

inverseImage(org.jmlspecs.models.JMLValueSet), inverse(), elementImage(org.jmlspecs.models.JMLType)

Specifications: non_null (class)pure

public normal_behavior
ensures \result .equals(this.inverse().elementImage(rv));

    implies_that

ensures \result != null&&!\result .containsNull;

inverseImage

public JMLValueSet inverseImage(non_null JMLValueSet rng)

Return a set of all the domain elements that relate to some element in the given set of range elements.

See Also:

inverseElementImage(org.jmlspecs.models.JMLType), inverse(), image(org.jmlspecs.models.JMLValueSet)

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(JMLType 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 JMLType dv,
                   nullable JMLType rv)

Tells whether this associates the given key to the given value.

See Also:

isDefinedAt(org.jmlspecs.models.JMLType), has(JMLValueValuePair)

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 JMLValueValuePair pair)

Tells whether this associates the given key to the given value.

See Also:

isDefinedAt(org.jmlspecs.models.JMLType), has(JMLType, JMLType)

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(org.jmlspecs.models.JMLType), has(JMLValueValuePair)

Specifications: pure

     also

public normal_behavior
ensures \result <==> obj != null&&obj instanceof org.jmlspecs.models.JMLValueValuePair&&this.has((org.jmlspecs.models.JMLValueValuePair)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.JMLValueToValueRelation&&((org.jmlspecs.models.JMLValueToValueRelation)\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.JMLValueToValueRelation;
ensures \result == this.theRelation.equals(((org.jmlspecs.models.JMLValueToValueRelation)obj).theRelation);

     also

public normal_behavior
requires obj == null||!(obj instanceof org.jmlspecs.models.JMLValueToValueRelation);
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 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()

Specifications: non_null (class)pure

public normal_behavior
ensures ( \forall org.jmlspecs.models.JMLType dv; ; \result .has(dv) == this.isDefinedAt(dv));

range

public JMLValueSet range()

Returns a set containing the range of this relation.

See Also:

rangeElements(), associations(), inverseElementImage(org.jmlspecs.models.JMLType), domain(), inverse()

Specifications: non_null (class)pure

public normal_behavior
ensures ( \forall org.jmlspecs.models.JMLType rv; ; \result .has(rv) == ( \exists org.jmlspecs.models.JMLType dv; ; this.elementImage(dv).has(rv)));

add

public JMLValueToValueRelation add(non_null JMLType dv,
                                   non_null JMLType 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.JMLValueValuePair)

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.JMLValueValuePair(dv, rv)));

insert

public JMLValueToValueRelation insert(non_null JMLValueValuePair 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, org.jmlspecs.models.JMLType)

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 JMLValueToValueRelation removeFromDomain(nullable 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(JMLValueValuePair), removeFromDomain(org.jmlspecs.models.JMLType)

Specifications: non_null (class)pure

public normal_behavior
ensures \result != null&&( \forall org.jmlspecs.models.JMLType val; this.domain().has(val); ( \forall org.jmlspecs.models.JMLType r; r != null; (this.elementImage(val).has(r) <==> \result .theRelation.has(new org.jmlspecs.models.JMLValueValuePair(val, r))&&!val.equals(dv))));

    implies_that

public normal_behavior
requires dv == null;
ensures \result != null&&\result .equals(this);

remove

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.

See Also:

removeFromDomain(org.jmlspecs.models.JMLType), remove(JMLType, JMLType), remove(JMLValueValuePair)

Specifications: non_null (class)pure

public normal_behavior
requires dv != null&&rv != null;
ensures \result .theRelation.equals(this.theRelation.remove(new org.jmlspecs.models.JMLValueValuePair(dv, rv)));

     also

requires dv == null||rv == null;
ensures \result != null&&\result .equals(this);

remove

public JMLValueToValueRelation remove(non_null JMLValueValuePair 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, JMLType), removeFromDomain(org.jmlspecs.models.JMLType)

Specifications: non_null (class)pure

public normal_behavior
requires pair != null;
ensures \result .theRelation.equals(this.theRelation.remove(pair));

compose

public JMLValueToValueRelation compose(non_null 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)

Specifications: non_null (class)pure

public normal_behavior
requires othRel != null;
ensures ( \forall org.jmlspecs.models.JMLValueValuePair pair; ; \result .theRelation.has(pair) == ( \exists org.jmlspecs.models.JMLType val; othRel.elementImage(pair.key).has(val); this.elementImage(val).has(pair.value)));

compose

public JMLObjectToValueRelation compose(non_null 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)

Specifications: non_null (class)pure

public normal_behavior
requires othRel != null;
ensures ( \forall org.jmlspecs.models.JMLValueValuePair pair; ; \result .theRelation.has(pair) == ( \exists org.jmlspecs.models.JMLType val; othRel.elementImage(pair.key).has(val); this.elementImage(val).has(pair.value)));

union

public JMLValueToValueRelation union(non_null JMLValueToValueRelation 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.JMLValueToValueRelation), intersection(org.jmlspecs.models.JMLValueToValueRelation)

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 JMLValueToValueRelation intersection(non_null JMLValueToValueRelation 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.JMLValueToValueRelation), union(org.jmlspecs.models.JMLValueToValueRelation)

Specifications: non_null (class)pure

public normal_behavior
requires othRel != null;
ensures \result .theRelation.equals(this.theRelation.intersection(othRel.theRelation));

difference

public JMLValueToValueRelation difference(non_null JMLValueToValueRelation 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.JMLValueToValueRelation), intersection(org.jmlspecs.models.JMLValueToValueRelation)

Specifications: non_null (class)pure

public normal_behavior
requires othRel != null;
ensures \result .theRelation.equals(this.theRelation.difference(othRel.theRelation));

restrictDomainTo

public JMLValueToValueRelation restrictDomainTo(non_null 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.JMLValueSet)

Specifications: non_null (class)pure

public normal_behavior
requires dom != null;
ensures ( \forall org.jmlspecs.models.JMLValueValuePair pair; pair != null; \result .theRelation.has(pair) == dom.has(pair.key)&&this.elementImage(pair.key).has(pair.value));

restrictRangeTo

public JMLValueToValueRelation restrictRangeTo(non_null JMLValueSet 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)

Specifications: non_null (class)pure

public normal_behavior
requires rng != null;
ensures ( \forall org.jmlspecs.models.JMLValueValuePair 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 JMLValueToValueRelationEnumerator 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.JMLValueToValueRelationEnumerator(this));

elements

public JMLValueToValueRelationEnumerator 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.JMLValueValuePair&&this.isDefinedAt(((org.jmlspecs.models.JMLValueValuePair)pv).key)&&this.elementImage(((org.jmlspecs.models.JMLValueValuePair)pv).key).has(((org.jmlspecs.models.JMLValueValuePair)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.JMLValueValuePair 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 org.jmlspecs.models.JMLType dv; this.domain().has(dv); \result .has(new org.jmlspecs.models.JMLValueValuePair(dv, this.elementImage(dv))));

imagePairs

public JMLValueToValueRelationImageEnumerator 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 org.jmlspecs.models.JMLType dv; this.domain().has(dv); \result .abstractValue().has(new org.jmlspecs.models.JMLValueValuePair(dv, this.elementImage(dv))));

domainElements

public JMLValueSetEnumerator 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 JMLValueSetEnumerator 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 JMLValueToValueMap 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(), JMLValueToValueMap

Specifications: non_null (class)pure

public normal_behavior
ensures ( \forall org.jmlspecs.models.JMLType dv; dv != null; (this.isDefinedAt(dv) == \result .isDefinedAt(dv))&&\result .elementImage(dv).isSubset(this.elementImage(dv))&&\result .elementImage(dv).int_size() == 1);