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