JML

org.jmlspecs.models
Class JMLValueToValueMap

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

public class JMLValueToValueMap
extends JMLValueToValueRelation

Maps (i.e., binary relations that are functional) from non-null elements of JMLType to non-null elements of JMLType. The first type, JMLType, 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 function that maps each element of the domain to some of elements of the range type.

This type is a subtype of JMLValueToValueRelation, and as such as can be treated as a binary relation or a set valued function also. See the documentation for JMLValueToValueRelation 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.34 $
Author:
Gary T. Leavens, Clyde Ruby
See Also:
JMLCollection, JMLType, JMLValueToValueRelation, JMLValueToValueRelationEnumerator, JMLValueToValueRelationImageEnumerator, JMLValueSet, JMLObjectSet, JMLObjectToObjectMap, JMLValueToObjectMap, JMLObjectToValueMap, JMLValueToValueMap, JMLValueToValueRelation.toFunction()

Field Summary
static JMLValueToValueMap EMPTY
          The empty JMLValueToValueMap.
 
Fields inherited from class org.jmlspecs.models.JMLValueToValueRelation
domain_, imagePairSet_, size_, TOO_BIG_TO_UNION
 
Constructor Summary
  JMLValueToValueMap()
          Initialize this map to be the empty mapping.
  JMLValueToValueMap(JMLType dv, JMLType rv)
          Initialize this map to be a mapping that maps the given domain element to the given range element.
protected JMLValueToValueMap(JMLValueSet ipset, JMLValueSet dom, int sz)
          Initialize this map based on the representation values given.
  JMLValueToValueMap(JMLValueValuePair pair)
          Initialize this map to be a mapping that maps the key in the given pair to the value in that pair.
 
Method Summary
 JMLType apply(JMLType dv)
          Return the range element corresponding to dv, if there is one.
 JMLValueToValueMap clashReplaceUnion(JMLValueToValueMap 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(JMLObjectToValueMap othMap)
          Return a new map that is the composition of this and the given map.
 JMLValueToValueMap compose(JMLValueToValueMap othMap)
          Return a new map that is the composition of this and the given map.
 JMLValueToValueMap disjointUnion(JMLValueToValueMap othMap)
          Return a map that is the disjoint union of this and othMap.
 JMLValueToValueMap extend(JMLType dv, JMLType rv)
          Return a new map that is like this but maps the given domain element to the given range element.
 JMLValueToValueMap extendUnion(JMLValueToValueMap 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.
 JMLValueToValueMap rangeRestrictedTo(JMLValueSet rng)
          Return a new map that is like this map but only contains associations that map to range elements in the given set.
 JMLValueToValueMap removeDomainElement(JMLType dv)
          Return a new map that is like this but has no association for the given domain element.
 JMLValueToValueMap restrictedTo(JMLValueSet dom)
          Return a new map that only maps elements in the given domain to the corresponding range elements in this map.
static JMLValueToValueMap singletonMap(JMLType dv, JMLType rv)
          Return the singleton map containing the given association.
static JMLValueToValueMap singletonMap(JMLValueValuePair pair)
          Return the singleton map containing the association described by the given pair.
 
Methods inherited from class org.jmlspecs.models.JMLValueToValueRelation
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 JMLValueToValueMap EMPTY
The empty JMLValueToValueMap.

See Also:
JMLValueToValueMap()
Constructor Detail

JMLValueToValueMap

public JMLValueToValueMap()
Initialize this map to be the empty mapping.

See Also:
EMPTY

JMLValueToValueMap

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

See Also:
singletonMap(JMLType, JMLType), JMLValueToValueMap(JMLValueValuePair)

JMLValueToValueMap

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

JMLValueToValueMap

protected JMLValueToValueMap(JMLValueSet ipset,
                             JMLValueSet dom,
                             int sz)
Initialize this map based on the representation values given.

Method Detail

singletonMap

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

See Also:
JMLValueToValueMap(JMLType, JMLType), singletonMap(JMLValueValuePair)

singletonMap

public static JMLValueToValueMap singletonMap(JMLValueValuePair pair)
Return the singleton map containing the association described by the given pair.

See Also:
JMLValueToValueMap(JMLValueValuePair), singletonMap(JMLType, JMLType)

isaFunction

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

Overrides:
isaFunction in class JMLValueToValueRelation

apply

public JMLType 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:
JMLValueToValueRelation.isDefinedAt(org.jmlspecs.models.JMLType), JMLValueToValueRelation.elementImage(org.jmlspecs.models.JMLType), JMLValueToValueRelation.image(org.jmlspecs.models.JMLValueSet)

clone

public Object clone()
Description copied from class: JMLValueToValueRelation
Return a clone of this object.

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

extend

public JMLValueToValueMap extend(JMLType dv,
                                 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:
JMLValueToValueRelation#insert(JMLType, JMLType)

removeDomainElement

public JMLValueToValueMap removeDomainElement(JMLType dv)
Return a new map that is like this but has no association for the given domain element.

See Also:
JMLValueToValueRelation.removeFromDomain(org.jmlspecs.models.JMLType)

compose

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

compose

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

restrictedTo

public JMLValueToValueMap restrictedTo(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.JMLValueSet), JMLValueToValueRelation.restrictDomainTo(org.jmlspecs.models.JMLValueSet)

rangeRestrictedTo

public JMLValueToValueMap rangeRestrictedTo(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.JMLValueSet), JMLValueToValueRelation.restrictRangeTo(org.jmlspecs.models.JMLValueSet)

extendUnion

public JMLValueToValueMap extendUnion(JMLValueToValueMap 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.JMLValueToValueMap, org.jmlspecs.models.JMLType), disjointUnion(org.jmlspecs.models.JMLValueToValueMap), JMLValueToValueRelation.union(org.jmlspecs.models.JMLValueToValueRelation)

clashReplaceUnion

public JMLValueToValueMap clashReplaceUnion(JMLValueToValueMap 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.JMLValueToValueMap), disjointUnion(org.jmlspecs.models.JMLValueToValueMap), JMLValueToValueRelation.union(org.jmlspecs.models.JMLValueToValueRelation)

disjointUnion

public JMLValueToValueMap disjointUnion(JMLValueToValueMap 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.JMLValueToValueMap), clashReplaceUnion(org.jmlspecs.models.JMLValueToValueMap, org.jmlspecs.models.JMLType), JMLValueToValueRelation.union(org.jmlspecs.models.JMLValueToValueRelation)

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.