org.jmlspecs.models
Class JMLEqualsToValueMap

java.lang.Object
  org.jmlspecs.models.JMLEqualsToValueRelation
      org.jmlspecs.models.JMLEqualsToValueMap

All Implemented Interfaces:

Cloneable, JMLCollection, JMLType, Serializable

public class JMLEqualsToValueMap

extends JMLEqualsToValueRelation

Maps (i.e., binary relations that are functional) from non-null elements of Object to non-null elements of JMLType. The first type, Object, is called the domain type of the map; the second type, JMLType, is called the range type of the map. A map can be seen as a set of pairs, of form (dv, rv), consisting of an element of the domain type, dv, and an element of the range type, rv. Alternatively, it can be seen as a partial function that maps each element of the domain to an element of the range type.

This type is a subtype of JMLEqualsToValueRelation, and as such as can be treated as a binary relation or a set valued function also. See the documentation for JMLEqualsToValueRelation and for the methods inherited from this supertype for more information.

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

Version:

$Revision: 1.35 $

Author:

Gary T. Leavens, Clyde Ruby

See Also:

JMLCollection, JMLType, JMLEqualsToValueRelation, JMLEqualsToValueRelationEnumerator, JMLEqualsToValueRelationImageEnumerator, JMLValueSet, JMLObjectSet, JMLObjectToObjectMap, JMLValueToObjectMap, JMLObjectToValueMap, JMLValueToValueMap, JMLEqualsToValueRelation.toFunction()

Class Specifications

public invariant this.isaFunction(); public invariant_redundantly ( \forall java.lang.Object dv; this.isDefinedAt(dv); this.elementImage(dv).int_size() == 1);

Specifications inherited from class JMLEqualsToValueRelation

public invariant ( \forall java.lang.Object obj; this.theRelation.has((org.jmlspecs.models.JMLType)obj); obj != null&&obj instanceof org.jmlspecs.models.JMLEqualsValuePair&&((org.jmlspecs.models.JMLEqualsValuePair)obj).key != null&&((org.jmlspecs.models.JMLEqualsValuePair)obj).value != null); public invariant_redundantly (* Every element of 'theRelation'is a JMLEqualsValuePair whose key and value are not null *); public invariant this.elementType == \type(org.jmlspecs.models.JMLEqualsValuePair); 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.JMLEqualsValuePair(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

 

Model fields inherited from class org.jmlspecs.models.JMLEqualsToValueRelation

theRelation

 

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
static JMLEqualsToValueMap	EMPTY           The empty JMLEqualsToValueMap.

 

Fields inherited from class org.jmlspecs.models.JMLEqualsToValueRelation

domain_, imagePairSet_, size_, TOO_BIG_TO_UNION

 

Constructor Summary
	JMLEqualsToValueMap()           Initialize this map to be the empty mapping.
	JMLEqualsToValueMap(non_null Object dv, non_null JMLType rv)           Initialize this map to be a mapping that maps the given domain element to the given range element.
	JMLEqualsToValueMap(non_null JMLEqualsValuePair pair)           Initialize this map to be a mapping that maps the key in the given pair to the value in that pair.
protected	JMLEqualsToValueMap(JMLValueSet ipset, JMLEqualsSet dom, int sz)           Initialize this map based on the representation values given.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

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

size

 

Method Summary
JMLType	apply(Object dv)           Return the range element corresponding to dv, if there is one.
JMLEqualsToValueMap	clashReplaceUnion(JMLEqualsToValueMap othMap, JMLType errval)           Return a new map that is like the union of the given map and this map, except that if both define a mapping for a given domain element, then each of these clashes is replaced by a mapping from the domain element in question to the given range element.
Object	clone()           Return a clone of this object.
JMLObjectToValueMap	compose(non_null JMLObjectToEqualsMap othMap)           Return a new map that is the composition of this and the given map.
JMLValueToValueMap	compose(non_null JMLValueToEqualsMap othMap)           Return a new map that is the composition of this and the given map.
JMLEqualsToValueMap	disjointUnion(non_null JMLEqualsToValueMap othMap)           Return a map that is the disjoint union of this and othMap.
JMLEqualsToValueMap	extend(non_null Object dv, non_null JMLType rv)           Return a new map that is like this but maps the given domain element to the given range element.
JMLEqualsToValueMap	extendUnion(non_null JMLEqualsToValueMap othMap)           Return a new map that is like the union of the given map and this map, except that if both define a mapping for a given domain element, then only the mapping in the given map is retained.
boolean	isaFunction()           Tells whether this relation is a function.
JMLEqualsToValueMap	rangeRestrictedTo(non_null JMLValueSet rng)           Return a new map that is like this map but only contains associations that map to range elements in the given set.
JMLEqualsToValueMap	removeDomainElement(Object dv)           Return a new map that is like this but has no association for the given domain element.
JMLEqualsToValueMap	restrictedTo(non_null JMLEqualsSet dom)           Return a new map that only maps elements in the given domain to the corresponding range elements in this map.
static JMLEqualsToValueMap	singletonMap(non_null Object dv, non_null JMLType rv)           Return the singleton map containing the given association.
static JMLEqualsToValueMap	singletonMap(non_null JMLEqualsValuePair pair)           Return the singleton map containing the association described by the given pair.

 

Methods inherited from class org.jmlspecs.models.JMLEqualsToValueRelation

add, associations, compose, compose, difference, domain, domainElements, elementImage, elements, equals, has, has, has, hashCode, image, imagePairs, imagePairSet, insert, int_size, intersection, inverse, inverseElementImage, inverseImage, isDefinedAt, isEmpty, iterator, range, rangeElements, remove, remove, removeFromDomain, restrictDomainTo, restrictRangeTo, singleton, singleton, toBag, toFunction, toSequence, toSet, toString, union

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Field Detail

EMPTY

public static final JMLEqualsToValueMap EMPTY

The empty JMLEqualsToValueMap.

See Also:

JMLEqualsToValueMap()

Specifications: non_null

JMLEqualsToValueMap

public JMLEqualsToValueMap()

Initialize this map to be the empty mapping.

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

JMLEqualsToValueMap

public JMLEqualsToValueMap(non_null Object dv,
                           non_null JMLType rv)

Initialize this map to be a mapping that maps the given domain element to the given range element.

See Also:

singletonMap(Object, JMLType), JMLEqualsToValueMap(JMLEqualsValuePair)

Specifications: (class)pure

public normal_behavior
requires dv != null&&rv != null;
assignable theRelation, owner, elementType, containsNull;
ensures (this.theRelation.int_size() == 1)&&this.elementImage(dv).has(rv);
ensures_redundantly this.isDefinedAt(dv);

JMLEqualsToValueMap

public JMLEqualsToValueMap(non_null JMLEqualsValuePair pair)

Initialize this map to be a mapping that maps the key in the given pair to the value in that pair.

See Also:

singletonMap(JMLEqualsValuePair), JMLEqualsToValueMap(Object, JMLType)

Specifications: (class)pure

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

JMLEqualsToValueMap

protected JMLEqualsToValueMap(JMLValueSet ipset,
                              JMLEqualsSet dom,
                              int sz)

Initialize this map based on the representation values given.

Specifications: (class)pure

requires ipset != null&&dom != null&&0 <= sz;
assignable theRelation, owner, elementType, containsNull;
ensures this.imagePairSet_ == ipset&&this.domain_ == dom&&this.size_ == sz;

singletonMap

public static JMLEqualsToValueMap singletonMap(non_null Object dv,
                                               non_null JMLType rv)

Return the singleton map containing the given association.

See Also:

JMLEqualsToValueMap(Object, JMLType), singletonMap(JMLEqualsValuePair)

Specifications: pure non_null

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

singletonMap

public static JMLEqualsToValueMap singletonMap(non_null JMLEqualsValuePair pair)

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

See Also:

JMLEqualsToValueMap(JMLEqualsValuePair), singletonMap(Object, JMLType)

Specifications: pure non_null

public normal_behavior
requires pair != null;
ensures \result != null&&\result .equals(new org.jmlspecs.models.JMLEqualsToValueMap(pair));

isaFunction

public boolean isaFunction()

Tells whether this relation is a function.

Overrides:

isaFunction in class JMLEqualsToValueRelation

Specifications: pure

     also

public normal_behavior
ensures \result ;

Specifications inherited from overridden method in class JMLEqualsToValueRelation:
       (class)pure

public normal_behavior
ensures \result == ( \forall java.lang.Object dv; this.isDefinedAt(dv); this.elementImage(dv).int_size() == 1);

apply

public JMLType apply(Object dv)
              throws JMLNoSuchElementException

Return the range element corresponding to dv, if there is one.

Parameters:

dv - the domain element for which an association is sought (the key to the table).

Throws:

JMLNoSuchElementException - when dv is not associated to any range element by this.

See Also:

JMLEqualsToValueRelation.isDefinedAt(java.lang.Object), JMLEqualsToValueRelation.elementImage(java.lang.Object), JMLEqualsToValueRelation.image(org.jmlspecs.models.JMLEqualsSet)

Specifications: non_null (class)pure

public normal_behavior
requires this.isDefinedAt(dv);
ensures this.elementImage(dv).has(\result );

     also

public exceptional_behavior
requires !this.isDefinedAt(dv);
signals_only org.jmlspecs.models.JMLNoSuchElementException;

clone

public Object clone()

Description copied from class: JMLEqualsToValueRelation

Return a clone of this object.

Specified by:

clone in interface JMLType

Overrides:

clone in class JMLEqualsToValueRelation

Specifications: pure non_null

     also

public normal_behavior
ensures \result instanceof org.jmlspecs.models.JMLEqualsToValueMap&&((org.jmlspecs.models.JMLEqualsToValueMap)\result ).theRelation.equals(this.theRelation);

Specifications inherited from overridden method in class JMLEqualsToValueRelation:
       (class)pure

     also

public normal_behavior
ensures \result instanceof org.jmlspecs.models.JMLEqualsToValueRelation&&((org.jmlspecs.models.JMLEqualsToValueRelation)\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);

extend

public JMLEqualsToValueMap extend(non_null Object dv,
                                  non_null JMLType rv)

Return a new map that is like this but maps the given domain element to the given range element. Any previously existing mapping for the domain element is removed first.

See Also:

JMLEqualsToValueRelation#insert(Object, JMLType)

Specifications: non_null (class)pure

public normal_behavior
requires dv != null&&rv != null;
requires !this.isDefinedAt(dv) ==> this.int_size() < 2147483647;
ensures \result .equals(this.removeDomainElement(dv).add(dv,rv));

removeDomainElement

public JMLEqualsToValueMap removeDomainElement(Object dv)

Return a new map that is like this but has no association for the given domain element.

See Also:

JMLEqualsToValueRelation.removeFromDomain(java.lang.Object)

Specifications: non_null (class)pure

public normal_behavior
ensures \result .equals(this.removeFromDomain(dv).toFunction());
ensures_redundantly !this.isDefinedAt(dv) ==> \result .equals(this);

compose

public JMLValueToValueMap compose(non_null JMLValueToEqualsMap othMap)

Return a new map that is the composition of this and the given map. The composition is done in the usual order; that is, if the given map maps x to y and this maps y to z, then the result maps x to z.

See Also:

compose(JMLObjectToEqualsMap)

Specifications: non_null (class)pure

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

Specifications inherited from overridden method compose(JMLValueToEqualsRelation othRel) in class JMLEqualsToValueRelation:
       non_null (class)pure

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

compose

public JMLObjectToValueMap compose(non_null JMLObjectToEqualsMap othMap)

Return a new map that is the composition of this and the given map. The composition is done in the usual order; that is, if the given map maps x to y and this maps y to z, then the result maps x to z.

See Also:

compose(JMLValueToEqualsMap)

Specifications: non_null (class)pure

public normal_behavior
requires othMap != null;
ensures ( \forall org.jmlspecs.models.JMLObjectValuePair pair; ; \result .theRelation.has(pair) == ( \exists java.lang.Object val; othMap.elementImage(pair.key).has(val); this.elementImage(val).has(pair.value)));

Specifications inherited from overridden method compose(JMLObjectToEqualsRelation othRel) in class JMLEqualsToValueRelation:
       non_null (class)pure

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

restrictedTo

public JMLEqualsToValueMap restrictedTo(non_null JMLEqualsSet dom)

Return a new map that only maps elements in the given domain to the corresponding range elements in this map.

See Also:

rangeRestrictedTo(org.jmlspecs.models.JMLValueSet), JMLEqualsToValueRelation.restrictDomainTo(org.jmlspecs.models.JMLEqualsSet)

Specifications: non_null (class)pure

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

rangeRestrictedTo

public JMLEqualsToValueMap rangeRestrictedTo(non_null JMLValueSet rng)

Return a new map that is like this map but only contains associations that map to range elements in the given set.

See Also:

restrictedTo(org.jmlspecs.models.JMLEqualsSet), JMLEqualsToValueRelation.restrictRangeTo(org.jmlspecs.models.JMLValueSet)

Specifications: non_null (class)pure

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

extendUnion

public JMLEqualsToValueMap extendUnion(non_null JMLEqualsToValueMap othMap)
                                throws IllegalStateException

Return a new map that is like the union of the given map and this map, except that if both define a mapping for a given domain element, then only the mapping in the given map is retained.

Throws:

IllegalStateException

See Also:

clashReplaceUnion(org.jmlspecs.models.JMLEqualsToValueMap, org.jmlspecs.models.JMLType), disjointUnion(org.jmlspecs.models.JMLEqualsToValueMap), JMLEqualsToValueRelation.union(org.jmlspecs.models.JMLEqualsToValueRelation)

Specifications: non_null (class)pure

public normal_behavior
requires othMap != null;
requires this.int_size() <= 2147483647-othMap.difference(this).int_size();
ensures ( \forall org.jmlspecs.models.JMLEqualsValuePair pair; ; \result .theRelation.has(pair) == othMap.elementImage(pair.key).has(pair.value)||(!othMap.isDefinedAt(pair.key)&&this.elementImage(pair.key).has(pair.value)));

clashReplaceUnion

public JMLEqualsToValueMap clashReplaceUnion(JMLEqualsToValueMap othMap,
                                             JMLType errval)
                                      throws IllegalStateException

Return a new map that is like the union of the given map and this map, except that if both define a mapping for a given domain element, then each of these clashes is replaced by a mapping from the domain element in question to the given range element.

Parameters:

othMap - the other map.

errval - the range element to use when clashes occur.

Throws:

IllegalStateException

See Also:

extendUnion(org.jmlspecs.models.JMLEqualsToValueMap), disjointUnion(org.jmlspecs.models.JMLEqualsToValueMap), JMLEqualsToValueRelation.union(org.jmlspecs.models.JMLEqualsToValueRelation)

Specifications: non_null (class)pure

public normal_behavior
requires othMap != null&&errval != null;
requires this.int_size() <= 2147483647-othMap.difference(this).int_size();
ensures ( \forall org.jmlspecs.models.JMLEqualsValuePair pair; ; \result .theRelation.has(pair) == (!othMap.isDefinedAt(pair.key)&&this.elementImage(pair.key).has(pair.value))||(!this.isDefinedAt(pair.key)&&othMap.elementImage(pair.key).has(pair.value))||(this.isDefinedAt(pair.key)&&othMap.isDefinedAt(pair.key)&&pair.value.equals(errval)));

    implies_that

requires othMap != null&&errval != null;

disjointUnion

public JMLEqualsToValueMap disjointUnion(non_null JMLEqualsToValueMap othMap)
                                  throws JMLMapException,
                                         IllegalStateException

Return a map that is the disjoint union of this and othMap.

Parameters:

othMap - the other mapping

Throws:

JMLMapException - the ranges of this and othMap have elements in common (i.e., when they interesect).

IllegalStateException

See Also:

extendUnion(org.jmlspecs.models.JMLEqualsToValueMap), clashReplaceUnion(org.jmlspecs.models.JMLEqualsToValueMap, org.jmlspecs.models.JMLType), JMLEqualsToValueRelation.union(org.jmlspecs.models.JMLEqualsToValueRelation)

Specifications: non_null (class)pure

public normal_behavior
requires othMap != null&&this.domain().intersection(othMap.domain()).isEmpty();
requires this.int_size() <= 2147483647-othMap.int_size();
ensures \result .equals(this.union(othMap));

     also

public exceptional_behavior
requires othMap != null&&!this.domain().intersection(othMap.domain()).isEmpty();
signals_only org.jmlspecs.models.JMLMapException;