0001: // @(#)$Id: JMLObjectToValueRelation.java 1.1.1.1 Mon, 09 May 2005 15:27:50 +0200 engelc $
0002:
0003: // Copyright (C) 1998, 1999, 2002 Iowa State University
0004:
0005: // This file is part of JML
0006:
0007: // JML is free software; you can redistribute it and/or modify
0008: // it under the terms of the GNU General Public License as published by
0009: // the Free Software Foundation; either version 2, or (at your option)
0010: // any later version.
0011:
0012: // JML is distributed in the hope that it will be useful,
0013: // but WITHOUT ANY WARRANTY; without even the implied warranty of
0014: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0015: // GNU General Public License for more details.
0016:
0017: // You should have received a copy of the GNU General Public License
0018: // along with JML; see the file COPYING. If not, write to
0019: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
0020:
0021: package org.jmlspecs.models;
0022:
0023: import java.util.Enumeration;
0024:
0025: /** Binary relations (or set-valued functions) from non-null elements
0026: * of {@link Object} to non-null elements of {@link
0027: * JMLType}. The first type, <kbd>Object</kbd>, is called
0028: * the domain type of the relation; the second type,
0029: * <kbd>JMLType</kbd>, is called the range type of the relation.
0030: * A relation can be seen as a set of pairs, of form <em>(dv,
0031: * rv)</em>, consisting of an element of the domain type,
0032: * <em>dv</em>, and an element of the range type, <em>rv</em>.
0033: * Alternatively, it can be seen as a set-valued function that
0034: * relates each element of the domain type to some set of elements of
0035: * the range type (a {@link JMLValueSet}).
0036: *
0037: * <p> This type considers elements <kbd>val</kbd> and <kbd>dv<kbd>
0038: * of the domain type, to be distinct just when
0039: * <kbd>val != dv</kbd>. It considers elements of
0040: * <kbd>r</kbd> and <kbd>rv</kbd> of the range type to be distinct
0041: * just when <kbd>!r.equals(rv)</kbd>. Cloning takes place for
0042: * the domain or range elements if the corresponding domain or range
0043: * type is {@link JMLType}.
0044: *
0045: * @version $Revision: 1.1.1.1 $
0046: * @author Gary T. Leavens
0047: * @author Clyde Ruby
0048: * @see JMLCollection
0049: * @see JMLType
0050: * @see JMLObjectToValueMap
0051: * @see JMLObjectToValueRelationEnumerator
0052: * @see JMLObjectToValueRelationImageEnumerator
0053: * @see JMLValueSet
0054: * @see JMLObjectSet
0055: * @see JMLObjectToObjectRelation
0056: * @see JMLValueToObjectRelation
0057: * @see JMLObjectToValueRelation
0058: * @see JMLValueToValueRelation
0059: */
0060: //-@ immutable
0061: public/*@ pure @*/class JMLObjectToValueRelation implements
0062: JMLCollection {
0063:
0064: /** The set of pairs of keys and values conceptually contained in
0065: * this object.
0066: */
0067: //@ public model JMLValueSet theRelation;
0068: /*@ public invariant
0069: @ (\forall Object obj; theRelation.has((JMLType)obj);
0070: @ obj != null
0071: @ && obj instanceof JMLObjectValuePair
0072: @ && ((JMLObjectValuePair)obj).key != null
0073: @ && ((JMLObjectValuePair)obj).value != null);
0074: @ public invariant_redundantly
0075: @ (* Every element of 'theRelation'is a JMLObjectValuePair
0076: @ whose key and value are not null *);
0077: @*/
0078:
0079: //@ public invariant elementType == \type(JMLObjectValuePair);
0080: //@ public invariant !containsNull;
0081: /** The set of elements in the domain of this relation.
0082: */
0083: protected final/*@ non_null @*/JMLObjectSet domain_;
0084: //@ in theRelation;
0085:
0086: /** The set representing the image pairs in the relation. The
0087: * elements of this set are JMLObjectValuePairs, which are all
0088: * non-null. Each such pair has a key which is an element in
0089: * domain_ and a value which is a JMLValueSet containing all of
0090: * the elements that the key of the pair is related to.
0091: */
0092: protected final/*@ non_null @*/JMLValueSet imagePairSet_;
0093: //@ in theRelation;
0094:
0095: /** The size (number of pairs) of this relation.
0096: */
0097: protected final int size_;
0098:
0099: //@ in theRelation;
0100:
0101: //@ protected represents theRelation <- toSet();
0102:
0103: /*@ protected invariant
0104: @ imagePairSet_.int_size() == domain_.int_size()
0105: @ && (\forall Object dv; dv != null && domain_.has(dv);
0106: @ imagePairSet_
0107: @ .has(new JMLObjectValuePair(dv, elementImage(dv))));
0108: @*/
0109: //@ protected invariant_redundantly imagePairSet_ == imagePairSet();
0110: //@ protected invariant size_ == theRelation.int_size();
0111: //@ protected invariant size_ >= 0;
0112: //@ public invariant owner == null;
0113: //************************* Constructors ********************************
0114: /** Initialize this to be an empty relation. That is, the value is
0115: * an empty set of pairs.
0116: * @see #EMPTY
0117: */
0118: /*@ public normal_behavior
0119: @ assignable theRelation, owner, elementType, containsNull;
0120: @ ensures theRelation.equals(new JMLValueSet());
0121: @ ensures_redundantly theRelation.isEmpty();
0122: @*/
0123: public JMLObjectToValueRelation() {
0124: domain_ = new JMLObjectSet();
0125: imagePairSet_ = new JMLValueSet();
0126: size_ = 0;
0127: }
0128:
0129: /** Initialize this to be a relation containing a single association
0130: * between the given domain and range elements.
0131: * @see #singleton(Object, JMLType)
0132: * @see #JMLObjectToValueRelation(JMLObjectValuePair)
0133: */
0134: /*@ public normal_behavior
0135: @ requires dv != null && rv != null;
0136: @ assignable theRelation, owner, elementType, containsNull;
0137: @ ensures theRelation.int_size() == 1;
0138: @ ensures elementImage(dv).has(rv);
0139: @ ensures_redundantly isDefinedAt(dv);
0140: @*/
0141: public JMLObjectToValueRelation(/*@ non_null @*/Object dv,
0142: /*@ non_null @*/JMLType rv) {
0143: size_ = 1;
0144: domain_ = new JMLObjectSet(dv);
0145: JMLValueSet img = new JMLValueSet(rv);
0146: imagePairSet_ = new JMLValueSet(new JMLObjectValuePair(dv, img));
0147: }
0148:
0149: /** Initialize this to be a relation containing a single association
0150: * given by the pair.
0151: * @see #singleton(JMLObjectValuePair)
0152: * @see #JMLObjectToValueRelation(Object, JMLType)
0153: */
0154: /*@ public normal_behavior
0155: @ requires pair != null;
0156: @ assignable theRelation, owner, elementType, containsNull;
0157: @ ensures theRelation.int_size() == 1 && theRelation.has(pair);
0158: @*/
0159: public JMLObjectToValueRelation(/*@ non_null @*/
0160: JMLObjectValuePair pair) {
0161: this (pair.key, pair.value);
0162: }
0163:
0164: /** Initialize this using the given representation.
0165: */
0166: /*@ protected normal_behavior
0167: @ requires ipset != null && dom != null && dom.int_size() <= sz;
0168: @ assignable theRelation, owner, elementType, containsNull;
0169: @ assignable_redundantly domain_, imagePairSet_, size_;
0170: @ ensures imagePairSet_ == ipset && domain_ == dom && size_ == sz;
0171: @
0172: @ implies_that
0173: @ requires ipset != null && dom != null && 0 <= sz;
0174: @ ensures imagePairSet_ == ipset && domain_ == dom && size_ == sz;
0175: @*/
0176: protected JMLObjectToValueRelation(
0177: /*@ non_null @*/JMLValueSet ipset,
0178: /*@ non_null @*/JMLObjectSet dom, int sz) {
0179: domain_ = dom;
0180: imagePairSet_ = ipset;
0181: size_ = sz;
0182: }
0183:
0184: //**************************** Static methods ****************************
0185:
0186: /** The empty JMLObjectToValueRelation.
0187: * @see #JMLObjectToValueRelation()
0188: */
0189: public static final/*@ non_null @*/JMLObjectToValueRelation EMPTY = new JMLObjectToValueRelation();
0190:
0191: /** Return the singleton relation containing the given association.
0192: * @see #singleton(JMLObjectValuePair)
0193: * @see #JMLObjectToValueRelation(Object, JMLType)
0194: */
0195: /*@ public normal_behavior
0196: @ requires dv != null && rv != null;
0197: @ ensures \result != null
0198: @ && \result.equals(new JMLObjectToValueRelation(dv, rv));
0199: @*/
0200: public static/*@ pure @*//*@ non_null @*/
0201: JMLObjectToValueRelation singleton(/*@ non_null @*/Object dv,
0202: /*@ non_null @*/JMLType rv) {
0203: return new JMLObjectToValueRelation(dv, rv);
0204: }
0205:
0206: /** Return the singleton relation containing the association
0207: * described by the given pair.
0208: * @see #singleton(Object, JMLType)
0209: * @see #JMLObjectToValueRelation(JMLObjectValuePair)
0210: */
0211: /*@ public normal_behavior
0212: @ requires pair != null;
0213: @ ensures \result != null
0214: @ && \result.equals(singleton(pair.key, pair.value));
0215: @*/
0216: public static/*@ pure @*//*@ non_null @*/
0217: JMLObjectToValueRelation singleton(
0218: /*@ non_null @*/JMLObjectValuePair pair) {
0219: return singleton(pair.key, pair.value);
0220: }
0221:
0222: //**************************** Observers **********************************
0223:
0224: /** Tells whether this relation is a function.
0225: * @see JMLObjectToValueMap
0226: */
0227: /*@ public normal_behavior
0228: @ ensures \result == (\forall Object dv; isDefinedAt(dv);
0229: @ elementImage(dv).int_size() == 1);
0230: @*/
0231: public boolean isaFunction() {
0232: return size_ == domain_.int_size();
0233: }
0234:
0235: /** Returns a set containing all the range elements that this
0236: * relation relates to the given domain element.
0237: * @see #image
0238: * @see JMLObjectToValueMap#apply
0239: */
0240: /*@ public normal_behavior
0241: @ ensures (\forall JMLObjectValuePair pair;
0242: @ theRelation.has(pair);
0243: @ pair.keyEquals(dv) ==> \result.has(pair.value));
0244: @ ensures (\forall JMLType o; \result.has(o);
0245: @ (\exists JMLObjectValuePair pair;
0246: @ theRelation.has(pair);
0247: @ pair.keyEquals(dv) && pair.valueEquals(o)));
0248: @ ensures_redundantly !isDefinedAt(dv) ==> \result.isEmpty();
0249: @
0250: @ implies_that
0251: @ ensures \result != null && !\result.containsNull;
0252: @*/
0253: public/*@ non_null @*/
0254: JMLValueSet elementImage(Object dv) {
0255: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0256: .imagePairs();
0257: JMLObjectValuePair imagePair;
0258: while (imagePairEnum.hasMoreElements()) {
0259: imagePair = imagePairEnum.nextImagePair();
0260: if (imagePair.keyEquals(dv)) {
0261: JMLValueSet res = (JMLValueSet) imagePair.value;
0262: return res;
0263: }
0264: }
0265: return new JMLValueSet();
0266: }
0267:
0268: /** Returns a set containing all the range elements that this
0269: * relation relates to the elements of the given set of domain elements.
0270: * @see #elementImage
0271: * @see #inverseImage
0272: * @see JMLObjectToValueMap#apply
0273: */
0274: /*@ public normal_behavior
0275: @ requires dom != null;
0276: @ ensures (\forall JMLType o; \result.has(o)
0277: @ <==> (\exists JMLObjectValuePair pair;
0278: @ theRelation.has(pair);
0279: @ dom.has(pair.key) && pair.valueEquals(o)));
0280: @ ensures_redundantly
0281: @ (\forall JMLObjectValuePair pair;
0282: @ theRelation.has(pair);
0283: @ dom.has(pair.key) ==> \result.has(pair.value));
0284: @
0285: @ implies_that
0286: @ ensures \result != null && !\result.containsNull;
0287: @*/
0288: public/*@ non_null @*/
0289: JMLValueSet image(/*@ non_null @*/JMLObjectSet dom) {
0290: JMLValueSet img = new JMLValueSet();
0291: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0292: .imagePairs();
0293: JMLObjectValuePair imagePair;
0294: //@ loop_invariant !img.containsNull;
0295: while (imagePairEnum.hasMoreElements()) {
0296: imagePair = imagePairEnum.nextImagePair();
0297: if (dom.has(imagePair.key)) {
0298: JMLValueSet ipv = (JMLValueSet) imagePair.value;
0299: img = img.union(ipv);
0300: }
0301: }
0302: return img;
0303: }
0304:
0305: /** Returns the inverse of this relation. The inverse is the
0306: * relation that relates each range element to the corresponding
0307: * domain element.
0308: * @see #inverseImage
0309: * @see #inverseElementImage
0310: */
0311: /*@ public normal_behavior
0312: @ ensures (\forall JMLValueObjectPair pair; ;
0313: @ \result.theRelation.has(pair)
0314: @ == elementImage(pair.value).has(pair.key));
0315: @*/
0316: public/*@ non_null @*/JMLValueToObjectRelation inverse() {
0317: JMLValueToObjectRelation invRel = new JMLValueToObjectRelation();
0318: JMLObjectToValueRelationEnumerator assocEnum = this
0319: .associations();
0320: JMLObjectValuePair pair;
0321: while (assocEnum.hasMoreElements()) {
0322: pair = assocEnum.nextPair();
0323: invRel = invRel.add(pair.value, pair.key);
0324: }
0325: return invRel;
0326: }
0327:
0328: /** Return a set of all the domain elements that relate to the
0329: * given range element.
0330: * @see #inverseImage
0331: * @see #inverse
0332: * @see #elementImage
0333: */
0334: /*@ public normal_behavior
0335: @ ensures \result.equals(inverse().elementImage(rv));
0336: @
0337: @ implies_that
0338: @ ensures \result != null && !\result.containsNull;
0339: @*/
0340: public/*@ non_null @*/
0341: JMLObjectSet inverseElementImage(JMLType rv) {
0342: JMLObjectSet invImg = new JMLObjectSet();
0343: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0344: .imagePairs();
0345: JMLObjectValuePair imagePair;
0346: //@ loop_invariant !invImg.containsNull;
0347: while (imagePairEnum.hasMoreElements()) {
0348: imagePair = imagePairEnum.nextImagePair();
0349: JMLValueSet img = (JMLValueSet) imagePair.value;
0350: if (img.has(rv)) {
0351: invImg = invImg.insert(imagePair.key);
0352: }
0353: }
0354: return invImg;
0355: }
0356:
0357: /** Return a set of all the domain elements that relate to some
0358: * element in the given set of range elements.
0359: * @see #inverseElementImage
0360: * @see #inverse
0361: * @see #image
0362: */
0363: /*@ public normal_behavior
0364: @ requires rng != null;
0365: @ ensures \result.equals(inverse().image(rng));
0366: @
0367: @ implies_that
0368: @ ensures \result != null && !\result.containsNull;
0369: @*/
0370: public/*@ non_null @*/
0371: JMLObjectSet inverseImage(/*@ non_null @*/JMLValueSet rng) {
0372: JMLObjectSet invImg = new JMLObjectSet();
0373: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0374: .imagePairs();
0375: JMLObjectValuePair imagePair;
0376: while (imagePairEnum.hasMoreElements()) {
0377: imagePair = imagePairEnum.nextImagePair();
0378: JMLValueSet img = (JMLValueSet) imagePair.value;
0379: if (!img.intersection(rng).isEmpty()) {
0380: invImg = invImg.insert(imagePair.key);
0381: }
0382: }
0383: return invImg;
0384: }
0385:
0386: /** Tells whether this relation associates any range element to the
0387: * given domain element.
0388: * @see #domain()
0389: */
0390: /*@ public normal_behavior
0391: @ ensures \result == (elementImage(dv).int_size() > 0);
0392: @ ensures_redundantly dv == null ==> !\result;
0393: @*/
0394: public boolean isDefinedAt(Object dv) {
0395: return domain_.has(dv);
0396: }
0397:
0398: /** Tells whether this associates the given key to the given value.
0399: * @see #isDefinedAt
0400: * @see #has(JMLObjectValuePair)
0401: */
0402: /*@ public normal_behavior
0403: @ ensures \result <==> domain().has(dv) && elementImage(dv).has(rv);
0404: @ ensures_redundantly dv == null || rv == null ==> !\result;
0405: @*/
0406: public/*@ pure @*/boolean has(Object dv, JMLType rv) {
0407: return domain_.has(dv) && elementImage(dv).has(rv);
0408: }
0409:
0410: /** Tells whether this associates the given key to the given value.
0411: * @see #isDefinedAt
0412: * @see #has(Object, JMLType)
0413: */
0414: /*@ public normal_behavior
0415: @ requires pair != null;
0416: @ ensures \result <==> has(pair.key, pair.value);
0417: @*/
0418: public/*@ pure @*/boolean has(
0419: /*@ non_null @*/JMLObjectValuePair pair) {
0420: return has(pair.key, pair.value);
0421: }
0422:
0423: /** Tells whether this associates the given key to the given value.
0424: * @see #isDefinedAt
0425: * @see #has(JMLObjectValuePair)
0426: */
0427: /*@ also
0428: @ public normal_behavior
0429: @ ensures \result <==>
0430: @ obj != null
0431: @ && obj instanceof JMLObjectValuePair
0432: @ && has((JMLObjectValuePair) obj);
0433: @*/
0434: public/*@ pure @*/boolean has(Object obj) {
0435: return obj != null && obj instanceof JMLObjectValuePair
0436: && has((JMLObjectValuePair) obj);
0437: }
0438:
0439: /** Tells whether the relation is empty.
0440: * @see #int_size()
0441: */
0442: /*@ public normal_behavior
0443: @ ensures \result == (theRelation.int_size() == 0);
0444: @*/
0445: public boolean isEmpty() {
0446: return size_ == 0;
0447: }
0448:
0449: /** Return a clone of this object.
0450: */
0451: /*@ also
0452: @ public normal_behavior
0453: @ ensures \result instanceof JMLObjectToValueRelation
0454: @ && ((JMLObjectToValueRelation)\result)
0455: @ .theRelation.equals(this.theRelation);
0456: @*/
0457: public Object clone() {
0458: return new JMLObjectToValueRelation(imagePairSet_, domain_,
0459: size_);
0460: }
0461:
0462: /** Test whether this object's value is equal to the given argument.
0463: */
0464: /*@ also
0465: @ public normal_behavior
0466: @ requires obj != null && obj instanceof JMLObjectToValueRelation;
0467: @ ensures \result ==
0468: @ this.theRelation.equals(
0469: @ ((JMLObjectToValueRelation)obj).theRelation);
0470: @ also
0471: @ public normal_behavior
0472: @ requires obj == null
0473: @ || !(obj instanceof JMLObjectToValueRelation);
0474: @ ensures !\result;
0475: @*/
0476: public boolean equals(Object obj) {
0477: if (obj == null || !(obj instanceof JMLObjectToValueRelation)) {
0478: return false;
0479: }
0480:
0481: JMLObjectToValueRelation rel = (JMLObjectToValueRelation) obj;
0482:
0483: if (size_ != rel.int_size()) {
0484: return false;
0485: }
0486:
0487: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0488: .imagePairs();
0489: JMLObjectValuePair imagePair;
0490: JMLValueSet img;
0491: while (imagePairEnum.hasMoreElements()) {
0492: imagePair = imagePairEnum.nextImagePair();
0493: img = (JMLValueSet) imagePair.value;
0494: if (!img.equals(rel.elementImage(imagePair.key))) {
0495: return false;
0496: }
0497: }
0498: return true;
0499: }
0500:
0501: /** Return a hash code for this object.
0502: */
0503: public int hashCode() {
0504: return imagePairSet_.hashCode();
0505: }
0506:
0507: /** Returns a set containing the domain of this relation.
0508: * @see #domainElements()
0509: * @see #associations()
0510: * @see #isDefinedAt
0511: * @see #image
0512: * @see #range()
0513: * @see #inverse()
0514: */
0515: /*@ public normal_behavior
0516: @ ensures (\forall Object dv; ;
0517: @ \result.has(dv) == isDefinedAt(dv));
0518: @*/
0519: public/*@ non_null @*/JMLObjectSet domain() {
0520: return domain_;
0521: }
0522:
0523: /** Returns a set containing the range of this relation.
0524: * @see #rangeElements()
0525: * @see #associations()
0526: * @see #inverseElementImage
0527: * @see #domain()
0528: * @see #inverse()
0529: */
0530: /*@ public normal_behavior
0531: @ ensures (\forall JMLType rv; ;
0532: @ \result.has(rv)
0533: @ == (\exists Object dv; ;
0534: @ elementImage(dv).has(rv))
0535: @ );
0536: @*/
0537: public/*@ non_null @*/JMLValueSet range() {
0538: JMLValueSet rangeSet = new JMLValueSet();
0539:
0540: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0541: .imagePairs();
0542: JMLObjectValuePair imagePair;
0543: JMLValueSet img;
0544: while (imagePairEnum.hasMoreElements()) {
0545: imagePair = imagePairEnum.nextImagePair();
0546: img = (JMLValueSet) imagePair.value;
0547: rangeSet = rangeSet.union(img);
0548: }
0549: return rangeSet;
0550: }
0551:
0552: private static final String TOO_BIG_TO_INSERT = "Cannot insert into a Relation with Integer.MAX_VALUE elements.";
0553:
0554: /** Return a relation that is just like this relation, except that
0555: * it also associates the given domain element to the given range
0556: * element.
0557: * @see #insert
0558: */
0559: /*@ public normal_behavior
0560: @ requires dv != null && rv != null;
0561: @ requires int_size() < Integer.MAX_VALUE || elementImage(dv).has(rv);
0562: @ ensures \result.theRelation.equals(
0563: @ this.theRelation.insert(new JMLObjectValuePair(dv, rv)));
0564: @*/
0565: public/*@ pure @*//*@ non_null @*/
0566: JMLObjectToValueRelation add(/*@ non_null @*/Object dv,
0567: /*@ non_null @*/JMLType rv) throws NullPointerException,
0568: IllegalStateException {
0569: if (rv == null) {
0570: throw new NullPointerException();
0571: }
0572:
0573: JMLValueSet newImagePairSet;
0574: JMLObjectSet newDom;
0575: int newSize;
0576: JMLValueSet img;
0577:
0578: if (!domain_.has(dv)) {
0579: if (size_ == Integer.MAX_VALUE) {
0580: throw new IllegalStateException(TOO_BIG_TO_INSERT);
0581: }
0582: newDom = domain_.insert(dv);
0583: newSize = size_ + 1;
0584: img = new JMLValueSet(rv);
0585: newImagePairSet = imagePairSet_
0586: .insert(new JMLObjectValuePair(dv, img));
0587: } else {
0588: newImagePairSet = new JMLValueSet();
0589: newDom = domain_;
0590: newSize = 0;
0591:
0592: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0593: .imagePairs();
0594: JMLObjectValuePair imagePair;
0595: while (imagePairEnum.hasMoreElements()) {
0596: imagePair = imagePairEnum.nextImagePair();
0597: img = (JMLValueSet) imagePair.value;
0598: if (imagePair.keyEquals(dv)) {
0599: img = img.insert(rv);
0600: }
0601: int size_inc = img.int_size();
0602: if (newSize <= Integer.MAX_VALUE - size_inc) {
0603: newSize = newSize + size_inc;
0604: } else {
0605: throw new IllegalStateException(TOO_BIG_TO_INSERT);
0606: }
0607: newImagePairSet = newImagePairSet
0608: .insert(new JMLObjectValuePair(imagePair.key,
0609: img));
0610: }
0611: }
0612: return new JMLObjectToValueRelation(newImagePairSet, newDom,
0613: newSize);
0614: }
0615:
0616: /** Return a relation that is just like this relation, except that
0617: * it also includes the association described by the given pair.
0618: * @see #add
0619: */
0620: /*@ public normal_behavior
0621: @ requires pair != null;
0622: @ requires int_size() < Integer.MAX_VALUE
0623: @ || elementImage(pair.key).has(pair.value);
0624: @ ensures \result.theRelation.equals(this.theRelation.insert(pair));
0625: @*/
0626: public/*@ non_null @*/
0627: JMLObjectToValueRelation insert(/*@ non_null @*/
0628: JMLObjectValuePair pair) throws IllegalStateException {
0629: return add(pair.key, pair.value);
0630: }
0631:
0632: /** Return a relation that is just like this relation, except that
0633: * it does not contain any association with the given domain element.
0634: * @see #remove(JMLObjectValuePair)
0635: * @see #removeFromDomain
0636: */
0637: /*@ public normal_behavior
0638: @ ensures \result != null
0639: @ && (\forall Object val; domain().has(val);
0640: @ (\forall JMLType r; r != null;
0641: @ (elementImage(val).has(r)
0642: @ <==> \result.theRelation
0643: @ .has(new JMLObjectValuePair(val,r))
0644: @ && val != dv)));
0645: @ implies_that
0646: @ public normal_behavior
0647: @ requires dv == null;
0648: @ ensures \result != null && \result.equals(this);
0649: @*/
0650: public/*@ non_null @*/
0651: JMLObjectToValueRelation removeFromDomain(Object dv) {
0652: if (!domain_.has(dv)) {
0653: return (this );
0654: }
0655:
0656: JMLValueSet newImagePairSet = new JMLValueSet();
0657: JMLObjectSet newDom = domain_.remove(dv);
0658: int newSize = 0;
0659:
0660: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0661: .imagePairs();
0662: JMLObjectValuePair imagePair;
0663: while (imagePairEnum.hasMoreElements()) {
0664: imagePair = imagePairEnum.nextImagePair();
0665: if (!imagePair.keyEquals(dv)) {
0666: newImagePairSet = newImagePairSet.insert(imagePair);
0667: JMLValueSet img = (JMLValueSet) imagePair.value;
0668: newSize = newSize + img.int_size();
0669: }
0670: }
0671: return new JMLObjectToValueRelation(newImagePairSet, newDom,
0672: newSize);
0673: }
0674:
0675: /** Return a relation that is just like this relation, except that
0676: * it does not contain the association, if any, between the given
0677: * domain and range elements.
0678: * @see #removeFromDomain
0679: * @see #remove(Object, JMLType)
0680: * @see #remove(JMLObjectValuePair)
0681: */
0682: /*@ public normal_behavior
0683: @ requires dv != null && rv != null;
0684: @ ensures \result.theRelation.equals(
0685: @ theRelation.remove(new JMLObjectValuePair(dv, rv)));
0686: @ also
0687: @ requires dv == null || rv == null;
0688: @ ensures \result != null && \result.equals(this);
0689: @*/
0690: public/*@ non_null @*/
0691: JMLObjectToValueRelation remove(Object dv, JMLType rv) {
0692: if (!domain_.has(dv)) {
0693: return (this );
0694: }
0695:
0696: JMLValueSet newImagePairSet = new JMLValueSet();
0697: JMLObjectSet newDom = domain_;
0698: int newSize = 0;
0699:
0700: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0701: .imagePairs();
0702: JMLObjectValuePair imagePair;
0703: JMLValueSet img;
0704: while (imagePairEnum.hasMoreElements()) {
0705: imagePair = imagePairEnum.nextImagePair();
0706: img = (JMLValueSet) imagePair.value;
0707: int imgSize = img.int_size();
0708: if (imagePair.keyEquals(dv)) {
0709: img = img.remove(rv);
0710: imgSize = img.int_size();
0711: if (imgSize > 0) {
0712: newImagePairSet = newImagePairSet
0713: .insert(new JMLObjectValuePair(dv, img));
0714: newSize = newSize + imgSize;
0715: } else {
0716: //@ assert imgSize == 0;
0717: newDom = newDom.remove(dv);
0718: }
0719: } else {
0720: newImagePairSet = newImagePairSet.insert(imagePair);
0721: newSize = newSize + imgSize;
0722: }
0723: }
0724: return new JMLObjectToValueRelation(newImagePairSet, newDom,
0725: newSize);
0726: }
0727:
0728: /** Return a relation that is just like this relation, except that
0729: * it does not contain association described by the given pair.
0730: * @see #remove(Object, JMLType)
0731: * @see #removeFromDomain
0732: */
0733: /*@ public normal_behavior
0734: @ requires pair != null;
0735: @ ensures \result.theRelation.equals(this.theRelation.remove(pair));
0736: @*/
0737: public/*@ non_null @*/
0738: JMLObjectToValueRelation remove(/*@ non_null @*/
0739: JMLObjectValuePair pair) {
0740: return remove(pair.key, pair.value);
0741: }
0742:
0743: /** Return a relation that is the composition of the given
0744: * relation and this relation. The composition is done in the
0745: * "usual" order, so that if the given relation relates x to y,
0746: * and this relation relates y to z, then the result relates x to
0747: * z.
0748: * @see #compose(JMLObjectToObjectRelation)
0749: */
0750: /*@ public normal_behavior
0751: @ requires othRel != null;
0752: @ ensures (\forall JMLValueValuePair pair; ;
0753: @ \result.theRelation.has(pair)
0754: @ == (\exists Object val;
0755: @ othRel.elementImage(pair.key).has(val);
0756: @ this.elementImage(val).has(pair.value)
0757: @ )
0758: @ );
0759: @*/
0760: public/*@ non_null @*/
0761: JMLValueToValueRelation compose(
0762: /*@ non_null @*/JMLValueToObjectRelation othRel) {
0763: JMLValueSet newImagePairSet = new JMLValueSet();
0764: JMLValueSet newDom = new JMLValueSet();
0765: int newSize = 0;
0766:
0767: JMLValueToObjectRelationImageEnumerator imagePairEnum = othRel
0768: .imagePairs();
0769: JMLValueValuePair imagePair;
0770: JMLObjectSet img1;
0771: JMLValueSet img2;
0772: int imgSize;
0773: while (imagePairEnum.hasMoreElements()) {
0774: imagePair = imagePairEnum.nextImagePair();
0775: img1 = (JMLObjectSet) imagePair.value;
0776: img2 = this .image(img1);
0777: imgSize = img2.int_size();
0778: if (imgSize > 0) {
0779: newImagePairSet = newImagePairSet
0780: .insert(new JMLValueValuePair(imagePair.key,
0781: img2));
0782: newSize = newSize + imgSize;
0783: newDom = newDom.insert(imagePair.key);
0784: }
0785: }
0786: return new JMLValueToValueRelation(newImagePairSet, newDom,
0787: newSize);
0788: }
0789:
0790: /** Return a relation that is the composition of the given
0791: * relation and this relation. The composition is done in the
0792: * "usual" order, so that if the given relation relates x to y,
0793: * and this relation relates y to z, then the result relates x to
0794: * z.
0795: * @see #compose(JMLValueToObjectRelation)
0796: */
0797: /*@ public normal_behavior
0798: @ requires othRel != null;
0799: @ ensures (\forall JMLValueValuePair pair; ;
0800: @ \result.theRelation.has(pair)
0801: @ == (\exists Object val;
0802: @ othRel.elementImage(pair.key).has(val);
0803: @ this.elementImage(val).has(pair.value)
0804: @ )
0805: @ );
0806: @*/
0807: public/*@ non_null @*/
0808: JMLObjectToValueRelation compose(
0809: /*@ non_null @*/JMLObjectToObjectRelation othRel) {
0810: JMLValueSet newImagePairSet = new JMLValueSet();
0811: JMLObjectSet newDom = new JMLObjectSet();
0812: int newSize = 0;
0813:
0814: JMLObjectToObjectRelationImageEnumerator imagePairEnum = othRel
0815: .imagePairs();
0816: JMLObjectValuePair imagePair;
0817: JMLObjectSet img1;
0818: JMLValueSet img2;
0819: int imgSize;
0820: while (imagePairEnum.hasMoreElements()) {
0821: imagePair = imagePairEnum.nextImagePair();
0822: img1 = (JMLObjectSet) imagePair.value;
0823: img2 = this .image(img1);
0824: imgSize = img2.int_size();
0825: if (imgSize > 0) {
0826: newImagePairSet = newImagePairSet
0827: .insert(new JMLObjectValuePair(imagePair.key,
0828: img2));
0829: newSize = newSize + imgSize;
0830: newDom = newDom.insert(imagePair.key);
0831: }
0832: }
0833: return new JMLObjectToValueRelation(newImagePairSet, newDom,
0834: newSize);
0835: }
0836:
0837: /** Return a relation that union of the this and the given relation.
0838: * This is the union of the sets of associations.
0839: * @see #difference
0840: * @see #intersection
0841: */
0842: /*@ public normal_behavior
0843: @ requires othRel != null;
0844: @ requires int_size()
0845: @ < Integer.MAX_VALUE - othRel.difference(this).int_size();
0846: @ ensures \result.theRelation.equals(
0847: @ this.theRelation.union(othRel.theRelation));
0848: @*/
0849: public/*@ non_null @*/
0850: JMLObjectToValueRelation union(
0851: /*@ non_null @*/JMLObjectToValueRelation othRel)
0852: throws IllegalStateException {
0853: JMLValueSet newImagePairSet = new JMLValueSet();
0854: JMLObjectSet newDom = domain_;
0855: int newSize = 0;
0856:
0857: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0858: .imagePairs();
0859: JMLObjectValuePair imagePair;
0860: JMLValueSet img;
0861: while (imagePairEnum.hasMoreElements()) {
0862: imagePair = imagePairEnum.nextImagePair();
0863: img = (JMLValueSet) imagePair.value;
0864: img = img.union(othRel.elementImage(imagePair.key));
0865: newImagePairSet = newImagePairSet
0866: .insert(new JMLObjectValuePair(imagePair.key, img));
0867: int size_inc = img.int_size();
0868: if (newSize <= Integer.MAX_VALUE - size_inc) {
0869: newSize = newSize + size_inc;
0870: } else {
0871: throw new IllegalStateException(TOO_BIG_TO_UNION);
0872: }
0873: }
0874: JMLObjectSet diffDom = othRel.domain().difference(this .domain_);
0875: imagePairEnum = othRel.imagePairs();
0876: while (imagePairEnum.hasMoreElements()) {
0877: imagePair = imagePairEnum.nextImagePair();
0878: if (diffDom.has(imagePair.key)) {
0879: newImagePairSet = newImagePairSet.insert(imagePair);
0880: newDom = newDom.insert(imagePair.key);
0881: img = (JMLValueSet) imagePair.value;
0882: int size_inc = img.int_size();
0883: if (newSize <= Integer.MAX_VALUE - size_inc) {
0884: newSize = newSize + size_inc;
0885: } else {
0886: throw new IllegalStateException(TOO_BIG_TO_UNION);
0887: }
0888: }
0889: }
0890: return new JMLObjectToValueRelation(newImagePairSet, newDom,
0891: newSize);
0892: }
0893:
0894: protected static final String TOO_BIG_TO_UNION = "Cannot make a union with more than Integer.MAX_VALUE elements.";
0895:
0896: /** Return a relation that is the intersection of this and the
0897: * given relation. This is the intersection of the sets of
0898: * associations.
0899: * @see #difference
0900: * @see #union
0901: */
0902: /*@ public normal_behavior
0903: @ requires othRel != null;
0904: @ ensures \result.theRelation.equals(
0905: @ this.theRelation.intersection(othRel.theRelation));
0906: @*/
0907: public/*@ non_null @*/
0908: JMLObjectToValueRelation intersection(
0909: /*@ non_null @*/JMLObjectToValueRelation othRel) {
0910: JMLValueSet newImagePairSet = new JMLValueSet();
0911: JMLObjectSet newDom = new JMLObjectSet();
0912: int newSize = 0;
0913:
0914: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0915: .imagePairs();
0916: JMLObjectValuePair imagePair;
0917: JMLValueSet img;
0918: while (imagePairEnum.hasMoreElements()) {
0919: imagePair = imagePairEnum.nextImagePair();
0920: img = (JMLValueSet) imagePair.value;
0921: img = img.intersection(othRel.elementImage(imagePair.key));
0922: if (!img.isEmpty()) {
0923: newImagePairSet = newImagePairSet
0924: .insert(new JMLObjectValuePair(imagePair.key,
0925: img));
0926: newDom = newDom.insert(imagePair.key);
0927: newSize = newSize + img.int_size();
0928: }
0929: }
0930: return new JMLObjectToValueRelation(newImagePairSet, newDom,
0931: newSize);
0932: }
0933:
0934: /** Return a relation that is the difference between this and the given
0935: * relation. This is the difference between the sets of
0936: * associations.
0937: * @see #difference
0938: * @see #intersection
0939: */
0940: /*@ public normal_behavior
0941: @ requires othRel != null;
0942: @ ensures \result.theRelation.equals(
0943: @ this.theRelation.difference(othRel.theRelation));
0944: @*/
0945: public/*@ non_null @*/
0946: JMLObjectToValueRelation difference(
0947: /*@ non_null @*/JMLObjectToValueRelation othRel) {
0948: JMLValueSet newImagePairSet = new JMLValueSet();
0949: JMLObjectSet newDom = new JMLObjectSet();
0950: int newSize = 0;
0951:
0952: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0953: .imagePairs();
0954: JMLObjectValuePair imagePair;
0955: JMLValueSet img;
0956: while (imagePairEnum.hasMoreElements()) {
0957: imagePair = imagePairEnum.nextImagePair();
0958: img = (JMLValueSet) imagePair.value;
0959: img = img.difference(othRel.elementImage(imagePair.key));
0960: if (!img.isEmpty()) {
0961: newImagePairSet = newImagePairSet
0962: .insert(new JMLObjectValuePair(imagePair.key,
0963: img));
0964: newDom = newDom.insert(imagePair.key);
0965: newSize = newSize + img.int_size();
0966: }
0967: }
0968: return new JMLObjectToValueRelation(newImagePairSet, newDom,
0969: newSize);
0970: }
0971:
0972: /** Return a relation that is like this relation except that its
0973: * domain is limited to just the elements of the given set.
0974: * @see #restrictRangeTo
0975: */
0976: /*@ public normal_behavior
0977: @ requires dom != null;
0978: @ ensures (\forall JMLObjectValuePair pair; pair != null;
0979: @ \result.theRelation.has(pair) == dom.has(pair.key)
0980: @ && elementImage(pair.key).has(pair.value)
0981: @ );
0982: @*/
0983: public/*@ non_null @*/
0984: JMLObjectToValueRelation restrictDomainTo(
0985: /*@ non_null @*/JMLObjectSet dom) {
0986: JMLValueSet newImagePairSet = new JMLValueSet();
0987: JMLObjectSet newDom = domain_.intersection(dom);
0988: int newSize = 0;
0989:
0990: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
0991: .imagePairs();
0992: JMLObjectValuePair imagePair;
0993: JMLValueSet img;
0994: while (imagePairEnum.hasMoreElements()) {
0995: imagePair = imagePairEnum.nextImagePair();
0996: if (newDom.has(imagePair.key)) {
0997: newImagePairSet = newImagePairSet.insert(imagePair);
0998: img = (JMLValueSet) imagePair.value;
0999: newSize = newSize + img.int_size();
1000: }
1001: }
1002: return new JMLObjectToValueRelation(newImagePairSet, newDom,
1003: newSize);
1004: }
1005:
1006: /** Return a relation that is like this relation except that its
1007: * range is limited to just the elements of the given set.
1008: * @see #restrictDomainTo
1009: */
1010: /*@ public normal_behavior
1011: @ requires rng != null;
1012: @ ensures (\forall JMLObjectValuePair pair; ;
1013: @ \result.theRelation.has(pair)
1014: @ == rng.has(pair.value)
1015: @ && elementImage(pair.key).has(pair.value)
1016: @ );
1017: @*/
1018: public/*@ non_null @*/
1019: JMLObjectToValueRelation restrictRangeTo(
1020: /*@ non_null @*/JMLValueSet rng) {
1021: JMLValueSet newImagePairSet = new JMLValueSet();
1022: JMLObjectSet newDom = new JMLObjectSet();
1023: int newSize = 0;
1024:
1025: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
1026: .imagePairs();
1027: JMLObjectValuePair imagePair;
1028: JMLValueSet img;
1029: while (imagePairEnum.hasMoreElements()) {
1030: imagePair = imagePairEnum.nextImagePair();
1031: img = ((JMLValueSet) imagePair.value).intersection(rng);
1032: if (!img.isEmpty()) {
1033: newImagePairSet = newImagePairSet
1034: .insert(new JMLObjectValuePair(imagePair.key,
1035: img));
1036: newDom = newDom.insert(imagePair.key);
1037: newSize = newSize + img.int_size();
1038: }
1039: }
1040: return new JMLObjectToValueRelation(newImagePairSet, newDom,
1041: newSize);
1042: }
1043:
1044: /** Return a string representation of this object.
1045: */
1046: /*@ also
1047: @ public normal_behavior
1048: @ ensures \result.equals(theRelation.toString());
1049: @*/
1050: public String toString() {
1051: return toSet().toString();
1052: }
1053:
1054: /** Return a enumerator for the set of associations that
1055: * conceptually make up this relation.
1056: * @see #elements()
1057: * @see #iterator()
1058: * @see #toSet()
1059: * @see #imagePairs()
1060: */
1061: /*@ public normal_behavior
1062: @ ensures \result != null &&
1063: @ \result.equals(new JMLObjectToValueRelationEnumerator(this));
1064: @*/
1065: public/*@ non_null @*/
1066: JMLObjectToValueRelationEnumerator associations() {
1067: return new JMLObjectToValueRelationEnumerator(this );
1068: }
1069:
1070: /** Return a enumerator for the set of associations that
1071: * conceptually make up this relation. This is a synonym for associations.
1072: * @see #associations()
1073: * @see #iterator()
1074: */
1075: /*@ public normal_behavior
1076: @ ensures \result != null &&
1077: @ \result.equals(associations());
1078: @*/
1079: public/*@ non_null @*/
1080: JMLObjectToValueRelationEnumerator elements() {
1081: return associations();
1082: }
1083:
1084: /** Returns an Iterator over the set of pairs conceptually
1085: * contained in this relation..
1086: * @see #associations()
1087: * @see #elements()
1088: */
1089: /*@ also
1090: @ public normal_behavior
1091: @ ensures \fresh(\result)
1092: @ && \result.equals(new JMLEnumerationToIterator(elements()));
1093: @*/
1094: public JMLIterator iterator() {
1095: return new JMLEnumerationToIterator(elements());
1096: }
1097:
1098: /** Return the set of all associations in this relation.
1099: * @see #associations()
1100: * @see #toBag()
1101: * @see #toSequence()
1102: */
1103: /*@ public normal_behavior
1104: @ ensures \result != null && \result.size == int_size()
1105: @ && (\forall JMLType pv; \result.has(pv);
1106: @ pv != null && pv instanceof JMLObjectValuePair
1107: @ && this.isDefinedAt(((JMLObjectValuePair)pv).key)
1108: @ && this.elementImage(((JMLObjectValuePair)pv).key)
1109: @ .has(((JMLObjectValuePair)pv).value));
1110: @
1111: @*/
1112: public/*@ non_null @*/JMLValueSet toSet() {
1113: JMLObjectToValueRelationEnumerator pairEnum = this
1114: .associations();
1115: JMLValueSet ret = new JMLValueSet();
1116: while (pairEnum.hasMoreElements()) {
1117: JMLObjectValuePair p = pairEnum.nextPair();
1118: ret = ret.insert(p);
1119: }
1120: return ret;
1121: }
1122:
1123: /** Return the bag of all associations in this relation.
1124: * @see #toSet()
1125: * @see #toSequence()
1126: */
1127: /*@ public normal_behavior
1128: @ ensures \result != null && \result.equals(toSet().toBag());
1129: @*/
1130: public/*@ non_null @*/JMLValueBag toBag() {
1131: JMLObjectToValueRelationEnumerator pairEnum = this
1132: .associations();
1133: JMLValueBag ret = new JMLValueBag();
1134: while (pairEnum.hasMoreElements()) {
1135: JMLObjectValuePair p = pairEnum.nextPair();
1136: ret = ret.insert(p);
1137: }
1138: return ret;
1139: }
1140:
1141: /** Return a sequence containing all associations in this relation.
1142: * @see #toSet()
1143: * @see #toBag()
1144: */
1145: /*@ public normal_behavior
1146: @ ensures \result != null
1147: @ && (\forall JMLObjectValuePair p;;
1148: @ \result.count(p) == 1 <==> this.has(p));
1149: @*/
1150: public/*@ non_null @*/JMLValueSequence toSequence() {
1151: JMLObjectToValueRelationEnumerator pairEnum = this
1152: .associations();
1153: JMLValueSequence ret = new JMLValueSequence();
1154: while (pairEnum.hasMoreElements()) {
1155: JMLObjectValuePair p = pairEnum.nextPair();
1156: ret = ret.insertFront(p);
1157: }
1158: return ret;
1159: }
1160:
1161: /** Return the set of image set pairs that make up this relation.
1162: * @see #imagePairs()
1163: * @see #toSet()
1164: */
1165: /*@ public normal_behavior
1166: @ ensures \result != null && \result.int_size() == domain().int_size()
1167: @ && (\forall Object dv; domain().has(dv);
1168: @ \result.has(
1169: @ new JMLObjectValuePair(dv, elementImage(dv))));
1170: @*/
1171: public/*@ non_null @*/JMLValueSet imagePairSet() {
1172: return imagePairSet_;
1173: }
1174:
1175: /** Return the set of domain image set pairs that make up this relation.
1176: * @see #imagePairSet()
1177: * @see #associations()
1178: * @see #toSet()
1179: */
1180: /*@ public normal_behavior
1181: @ ensures \result != null
1182: @ && \result.abstractValue().int_size() == domain().int_size()
1183: @ && (\forall Object dv; domain().has(dv);
1184: @ \result.abstractValue().has(
1185: @ new JMLObjectValuePair(dv, elementImage(dv))));
1186: @*/
1187: public/*@ non_null @*/
1188: JMLObjectToValueRelationImageEnumerator imagePairs() {
1189: return new JMLObjectToValueRelationImageEnumerator(this );
1190: }
1191:
1192: /** Return a enumerator for the set that is the domain of this
1193: * relation.
1194: * @see #domain()
1195: * @see #rangeElements()
1196: */
1197: /*@ public normal_behavior
1198: @ ensures \result.equals(domain().elements());
1199: @*/
1200: public/*@ non_null @*/JMLObjectSetEnumerator domainElements() {
1201: return domain_.elements();
1202: }
1203:
1204: /** Return a enumerator for the set that is the range of this
1205: * relation. (This was formerly called "elements").
1206: * @see #range()
1207: * @see #domainElements()
1208: */
1209: /*@ public normal_behavior
1210: @ ensures \result.equals(range().elements());
1211: @*/
1212: public/*@ non_null @*/JMLValueSetEnumerator rangeElements() {
1213: return range().elements();
1214: }
1215:
1216: /** Return the number of associations in this relation.
1217: */
1218: /*@ also
1219: @ public normal_behavior
1220: @ ensures \result == theRelation.int_size();
1221: @*/
1222: public int int_size() {
1223: return size_;
1224: }
1225:
1226: /** Return a map that is contained in this relation. If this
1227: * relation is a function, then this method can be seen as a type
1228: * conversion which does not make a change to the abstract value.
1229: * However, if this relation is not a function, then this method
1230: * chooses a function contained in this relation from among the
1231: * possibilities available.
1232: * @see #isaFunction
1233: * @see JMLObjectToValueMap
1234: */
1235: /*@ public normal_behavior
1236: @ ensures (\forall Object dv; dv != null;
1237: @ (this.isDefinedAt(dv) == \result.isDefinedAt(dv))
1238: @ && \result.elementImage(dv).isSubset(this.elementImage(dv))
1239: @ && \result.elementImage(dv).int_size() == 1);
1240: @*/
1241: public/*@ non_null @*/JMLObjectToValueMap toFunction() {
1242: JMLObjectSet newDom = domain_;
1243: int newSize = domain_.int_size();
1244:
1245: JMLValueSet newImagePairSet = imagePairSet_;
1246:
1247: if (newSize != size_) {
1248: // Have to restrict the result to be a function
1249: JMLObjectToValueRelationImageEnumerator imagePairEnum = this
1250: .imagePairs();
1251: newImagePairSet = new JMLValueSet();
1252: JMLObjectValuePair imagePair;
1253: JMLValueSet img;
1254: while (imagePairEnum.hasMoreElements()) {
1255: imagePair = imagePairEnum.nextImagePair();
1256: img = (JMLValueSet) imagePair.value;
1257: Enumeration imgEnum = img.elements();
1258: Object o = imgEnum.nextElement();
1259: if (o == null) {
1260: img = new JMLValueSet(null);
1261: } else {
1262: JMLType rv = (JMLType) o;
1263: img = new JMLValueSet(rv);
1264: }
1265: newImagePairSet = newImagePairSet
1266: .insert(new JMLObjectValuePair(imagePair.key,
1267: img));
1268: }
1269: }
1270: return new JMLObjectToValueMap(newImagePairSet, newDom, newSize);
1271: }
1272: }
|