JML

org.jmlspecs.models
Class JMLValueToObjectMap

java.lang.Object
  extended byorg.jmlspecs.models.JMLValueToObjectRelation
      extended byorg.jmlspecs.models.JMLValueToObjectMap
All Implemented Interfaces:
Cloneable, JMLCollection, JMLType, Serializable

public class JMLValueToObjectMap
extends JMLValueToObjectRelation

Maps (i.e., binary relations that are functional) from non-null elements of JMLType to non-null elements of Object. The first type, JMLType, is called the domain type of the map; the second type, Object, 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 JMLValueToObjectRelation, and as such as can be treated as a binary relation or a set valued function also. See the documentation for JMLValueToObjectRelation 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, JMLValueToObjectRelation, JMLValueToObjectRelationEnumerator, JMLValueToObjectRelationImageEnumerator, JMLValueSet, JMLObjectSet, JMLObjectToObjectMap, JMLValueToObjectMap, JMLObjectToValueMap, JMLValueToValueMap, JMLValueToObjectRelation.toFunction()

Class Specifications
public invariant this.isaFunction();
public invariant_redundantly ( \forall org.jmlspecs.models.JMLType dv; this.isDefinedAt(dv); this.elementImage(dv).int_size() == 1);

Specifications inherited from class JMLValueToObjectRelation
public invariant ( \forall java.lang.Object obj; this.theRelation.has((org.jmlspecs.models.JMLType)obj); obj != null&&obj instanceof org.jmlspecs.models.JMLValueObjectPair&&((org.jmlspecs.models.JMLValueObjectPair)obj).key != null&&((org.jmlspecs.models.JMLValueObjectPair)obj).value != null);
public invariant_redundantly (* Every element of 'theRelation'is a JMLValueObjectPair whose key and value are not null *);
public invariant this.elementType == \type(org.jmlspecs.models.JMLValueObjectPair);
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
 
Model fields inherited from class org.jmlspecs.models.JMLValueToObjectRelation
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 JMLValueToObjectMap EMPTY
          The empty JMLValueToObjectMap.
 
Fields inherited from class org.jmlspecs.models.JMLValueToObjectRelation
domain_, imagePairSet_, size_, TOO_BIG_TO_UNION
 
Constructor Summary
  JMLValueToObjectMap()
          Initialize this map to be the empty mapping.
  JMLValueToObjectMap(non_null JMLType dv, non_null Object rv)
          Initialize this map to be a mapping that maps the given domain element to the given range element.
  JMLValueToObjectMap(non_null JMLValueObjectPair pair)
          Initialize this map to be a mapping that maps the key in the given pair to the value in that pair.
protected JMLValueToObjectMap(JMLValueSet ipset, JMLValueSet 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
 Object apply(JMLType dv)
          Return the range element corresponding to dv, if there is one.
 JMLValueToObjectMap clashReplaceUnion(JMLValueToObjectMap othMap, Object 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.
 JMLObjectToObjectMap compose(non_null JMLObjectToValueMap othMap)
          Return a new map that is the composition of this and the given map.
 JMLValueToObjectMap compose(non_null JMLValueToValueMap othMap)
          Return a new map that is the composition of this and the given map.
 JMLValueToObjectMap disjointUnion(non_null JMLValueToObjectMap othMap)
          Return a map that is the disjoint union of this and othMap.
 JMLValueToObjectMap extend(non_null JMLType dv, non_null Object rv)
          Return a new map that is like this but maps the given domain element to the given range element.
 JMLValueToObjectMap extendUnion(non_null JMLValueToObjectMap 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.
 JMLValueToObjectMap rangeRestrictedTo(non_null JMLObjectSet rng)
          Return a new map that is like this map but only contains associations that map to range elements in the given set.
 JMLValueToObjectMap removeDomainElement(JMLType dv)
          Return a new map that is like this but has no association for the given domain element.
 JMLValueToObjectMap restrictedTo(non_null JMLValueSet dom)
          Return a new map that only maps elements in the given domain to the corresponding range elements in this map.
static JMLValueToObjectMap singletonMap(non_null JMLType dv, non_null Object rv)
          Return the singleton map containing the given association.
static JMLValueToObjectMap singletonMap(non_null JMLValueObjectPair pair)
          Return the singleton map containing the association described by the given pair.
 
Methods inherited from class org.jmlspecs.models.JMLValueToObjectRelation
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 JMLValueToObjectMap EMPTY
The empty JMLValueToObjectMap.

See Also:
JMLValueToObjectMap()
Specifications: non_null
Constructor Detail

JMLValueToObjectMap

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

JMLValueToObjectMap

public JMLValueToObjectMap(non_null JMLType dv,
                           non_null Object rv)
Initialize this map to be a mapping that maps the given domain element to the given range element.

See Also:
singletonMap(JMLType, Object), JMLValueToObjectMap(JMLValueObjectPair)
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);

JMLValueToObjectMap

public JMLValueToObjectMap(non_null JMLValueObjectPair 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(JMLValueObjectPair), JMLValueToObjectMap(JMLType, Object)
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);

JMLValueToObjectMap

protected JMLValueToObjectMap(JMLValueSet ipset,
                              JMLValueSet 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;
Method Detail

singletonMap

public static JMLValueToObjectMap singletonMap(non_null JMLType dv,
                                               non_null Object rv)
Return the singleton map containing the given association.

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

singletonMap

public static JMLValueToObjectMap singletonMap(non_null JMLValueObjectPair pair)
Return the singleton map containing the association described by the given pair.

See Also:
JMLValueToObjectMap(JMLValueObjectPair), singletonMap(JMLType, Object)
Specifications: pure non_null
public normal_behavior
requires pair != null;
ensures \result != null&&\result .equals(new org.jmlspecs.models.JMLValueToObjectMap(pair));

isaFunction

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

Overrides:
isaFunction in class JMLValueToObjectRelation
Specifications: pure
     also
public normal_behavior
ensures \result ;
Specifications inherited from overridden method in class JMLValueToObjectRelation:
       (class)pure
public normal_behavior
ensures \result == ( \forall org.jmlspecs.models.JMLType dv; this.isDefinedAt(dv); this.elementImage(dv).int_size() == 1);

apply

public Object apply(JMLType 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:
JMLValueToObjectRelation.isDefinedAt(org.jmlspecs.models.JMLType), JMLValueToObjectRelation.elementImage(org.jmlspecs.models.JMLType), JMLValueToObjectRelation.image(org.jmlspecs.models.JMLValueSet)
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: JMLValueToObjectRelation
Return a clone of this object.

Specified by:
clone in interface JMLType
Overrides:
clone in class JMLValueToObjectRelation
Specifications: pure non_null
     also
public normal_behavior
ensures \result instanceof org.jmlspecs.models.JMLValueToObjectMap&&((org.jmlspecs.models.JMLValueToObjectMap)\result ).theRelation.equals(this.theRelation);
Specifications inherited from overridden method in class JMLValueToObjectRelation:
       (class)pure
     also
public normal_behavior
ensures \result instanceof org.jmlspecs.models.JMLValueToObjectRelation&&((org.jmlspecs.models.JMLValueToObjectRelation)\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 JMLValueToObjectMap extend(non_null JMLType dv,
                                  non_null Object 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:
JMLValueToObjectRelation#insert(JMLType, Object)
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 JMLValueToObjectMap removeDomainElement(JMLType dv)
Return a new map that is like this but has no association for the given domain element.

See Also:
JMLValueToObjectRelation.removeFromDomain(org.jmlspecs.models.JMLType)
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 JMLValueToObjectMap compose(non_null JMLValueToValueMap 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(JMLObjectToValueMap)
Specifications: non_null (class)pure
public normal_behavior
requires othMap != null;
ensures ( \forall org.jmlspecs.models.JMLValueObjectPair pair; ; \result .theRelation.has(pair) == ( \exists org.jmlspecs.models.JMLType val; othMap.elementImage(pair.key).has(val); this.elementImage(val).has(pair.value)));
Specifications inherited from overridden method compose(JMLValueToValueRelation othRel) in class JMLValueToObjectRelation:
       non_null (class)pure
public normal_behavior
requires othRel != null;
ensures ( \forall org.jmlspecs.models.JMLValueObjectPair 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 JMLObjectToObjectMap compose(non_null JMLObjectToValueMap 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(JMLValueToValueMap)
Specifications: non_null (class)pure
public normal_behavior
requires othMap != null;
ensures ( \forall org.jmlspecs.models.JMLObjectObjectPair pair; ; \result .theRelation.has(pair) == ( \exists org.jmlspecs.models.JMLType val; othMap.elementImage(pair.key).has(val); this.elementImage(val).has(pair.value)));
Specifications inherited from overridden method compose(JMLObjectToValueRelation othRel) in class JMLValueToObjectRelation:
       non_null (class)pure
public normal_behavior
requires othRel != null;
ensures ( \forall org.jmlspecs.models.JMLValueObjectPair pair; ; \result .theRelation.has(pair) == ( \exists org.jmlspecs.models.JMLType val; othRel.elementImage(pair.key).has(val); this.elementImage(val).has(pair.value)));

restrictedTo

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

rangeRestrictedTo

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

extendUnion

public JMLValueToObjectMap extendUnion(non_null JMLValueToObjectMap 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.JMLValueToObjectMap, java.lang.Object), disjointUnion(org.jmlspecs.models.JMLValueToObjectMap), JMLValueToObjectRelation.union(org.jmlspecs.models.JMLValueToObjectRelation)
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.JMLValueObjectPair 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 JMLValueToObjectMap clashReplaceUnion(JMLValueToObjectMap othMap,
                                             Object 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.JMLValueToObjectMap), disjointUnion(org.jmlspecs.models.JMLValueToObjectMap), JMLValueToObjectRelation.union(org.jmlspecs.models.JMLValueToObjectRelation)
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.JMLValueObjectPair 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 == (errval)));
    implies_that
requires othMap != null&&errval != null;

disjointUnion

public JMLValueToObjectMap disjointUnion(non_null JMLValueToObjectMap 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.JMLValueToObjectMap), clashReplaceUnion(org.jmlspecs.models.JMLValueToObjectMap, java.lang.Object), JMLValueToObjectRelation.union(org.jmlspecs.models.JMLValueToObjectRelation)
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;

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.