0001: // @(#)$Id: JMLValueToEqualsRelation.java 1.2 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 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 JMLEqualsSet}).
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.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.2 $
0046: * @author Gary T. Leavens
0047: * @author Clyde Ruby
0048: * @see JMLCollection
0049: * @see JMLType
0050: * @see JMLValueToEqualsMap
0051: * @see JMLValueToEqualsRelationEnumerator
0052: * @see JMLValueToEqualsRelationImageEnumerator
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 JMLValueToEqualsRelation 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 JMLValueEqualsPair
0072: @ && ((JMLValueEqualsPair)obj).key != null
0073: @ && ((JMLValueEqualsPair)obj).value != null);
0074: @ public invariant_redundantly
0075: @ (* Every element of 'theRelation'is a JMLValueEqualsPair
0076: @ whose key and value are not null *);
0077: @*/
0078:
0079: //@ public invariant elementType == \type(JMLValueEqualsPair);
0080: //@ public invariant !containsNull;
0081: /** The set of elements in the domain of this relation.
0082: */
0083: protected final/*@ non_null @*/JMLValueSet domain_;
0084: //@ in theRelation;
0085:
0086: /** The set representing the image pairs in the relation. The
0087: * elements of this set are JMLValueValuePairs, 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 JMLEqualsSet 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 JMLType dv; dv != null && domain_.has(dv);
0106: @ imagePairSet_
0107: @ .has(new JMLValueValuePair(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 JMLValueToEqualsRelation() {
0124: domain_ = new JMLValueSet();
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(JMLType, Object)
0132: * @see #JMLValueToEqualsRelation(JMLValueEqualsPair)
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 JMLValueToEqualsRelation(/*@ non_null @*/JMLType dv,
0142: /*@ non_null @*/Object rv) {
0143: size_ = 1;
0144: domain_ = new JMLValueSet(dv);
0145: JMLEqualsSet img = new JMLEqualsSet(rv);
0146: imagePairSet_ = new JMLValueSet(new JMLValueValuePair(dv, img));
0147: }
0148:
0149: /** Initialize this to be a relation containing a single association
0150: * given by the pair.
0151: * @see #singleton(JMLValueEqualsPair)
0152: * @see #JMLValueToEqualsRelation(JMLType, Object)
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 JMLValueToEqualsRelation(/*@ non_null @*/
0160: JMLValueEqualsPair 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 JMLValueToEqualsRelation(
0177: /*@ non_null @*/JMLValueSet ipset,
0178: /*@ non_null @*/JMLValueSet dom, int sz) {
0179: domain_ = dom;
0180: imagePairSet_ = ipset;
0181: size_ = sz;
0182: }
0183:
0184: //**************************** Static methods ****************************
0185:
0186: /** The empty JMLValueToEqualsRelation.
0187: * @see #JMLValueToEqualsRelation()
0188: */
0189: public static final/*@ non_null @*/JMLValueToEqualsRelation EMPTY = new JMLValueToEqualsRelation();
0190:
0191: /** Return the singleton relation containing the given association.
0192: * @see #singleton(JMLValueEqualsPair)
0193: * @see #JMLValueToEqualsRelation(JMLType, Object)
0194: */
0195: /*@ public normal_behavior
0196: @ requires dv != null && rv != null;
0197: @ ensures \result != null
0198: @ && \result.equals(new JMLValueToEqualsRelation(dv, rv));
0199: @*/
0200: public static/*@ pure @*//*@ non_null @*/
0201: JMLValueToEqualsRelation singleton(/*@ non_null @*/JMLType dv,
0202: /*@ non_null @*/Object rv) {
0203: return new JMLValueToEqualsRelation(dv, rv);
0204: }
0205:
0206: /** Return the singleton relation containing the association
0207: * described by the given pair.
0208: * @see #singleton(JMLType, Object)
0209: * @see #JMLValueToEqualsRelation(JMLValueEqualsPair)
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: JMLValueToEqualsRelation singleton(
0218: /*@ non_null @*/JMLValueEqualsPair pair) {
0219: return singleton(pair.key, pair.value);
0220: }
0221:
0222: //**************************** Observers **********************************
0223:
0224: /** Tells whether this relation is a function.
0225: * @see JMLValueToEqualsMap
0226: */
0227: /*@ public normal_behavior
0228: @ ensures \result == (\forall JMLType 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 JMLValueToEqualsMap#apply
0239: */
0240: /*@ public normal_behavior
0241: @ ensures (\forall JMLValueEqualsPair pair;
0242: @ theRelation.has(pair);
0243: @ pair.keyEquals(dv) ==> \result.has(pair.value));
0244: @ ensures (\forall Object o; \result.has(o);
0245: @ (\exists JMLValueEqualsPair 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: JMLEqualsSet elementImage(JMLType dv) {
0255: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0256: .imagePairs();
0257: JMLValueValuePair imagePair;
0258: while (imagePairEnum.hasMoreElements()) {
0259: imagePair = imagePairEnum.nextImagePair();
0260: if (imagePair.keyEquals(dv)) {
0261: JMLEqualsSet res = (JMLEqualsSet) imagePair.value;
0262: return res;
0263: }
0264: }
0265: return new JMLEqualsSet();
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 JMLValueToEqualsMap#apply
0273: */
0274: /*@ public normal_behavior
0275: @ requires dom != null;
0276: @ ensures (\forall Object o; \result.has(o)
0277: @ <==> (\exists JMLValueEqualsPair pair;
0278: @ theRelation.has(pair);
0279: @ dom.has(pair.key) && pair.valueEquals(o)));
0280: @ ensures_redundantly
0281: @ (\forall JMLValueEqualsPair 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: JMLEqualsSet image(/*@ non_null @*/JMLValueSet dom) {
0290: JMLEqualsSet img = new JMLEqualsSet();
0291: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0292: .imagePairs();
0293: JMLValueValuePair imagePair;
0294: //@ loop_invariant !img.containsNull;
0295: while (imagePairEnum.hasMoreElements()) {
0296: imagePair = imagePairEnum.nextImagePair();
0297: if (dom.has(imagePair.key)) {
0298: JMLEqualsSet ipv = (JMLEqualsSet) 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 JMLEqualsValuePair pair; ;
0313: @ \result.theRelation.has(pair)
0314: @ == elementImage(pair.value).has(pair.key));
0315: @*/
0316: public/*@ non_null @*/JMLEqualsToValueRelation inverse() {
0317: JMLEqualsToValueRelation invRel = new JMLEqualsToValueRelation();
0318: JMLValueToEqualsRelationEnumerator assocEnum = this
0319: .associations();
0320: JMLValueEqualsPair 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: JMLValueSet inverseElementImage(Object rv) {
0342: JMLValueSet invImg = new JMLValueSet();
0343: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0344: .imagePairs();
0345: JMLValueValuePair imagePair;
0346: //@ loop_invariant !invImg.containsNull;
0347: while (imagePairEnum.hasMoreElements()) {
0348: imagePair = imagePairEnum.nextImagePair();
0349: JMLEqualsSet img = (JMLEqualsSet) 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: JMLValueSet inverseImage(/*@ non_null @*/JMLEqualsSet rng) {
0372: JMLValueSet invImg = new JMLValueSet();
0373: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0374: .imagePairs();
0375: JMLValueValuePair imagePair;
0376: //@ loop_invariant !invImg.containsNull;
0377: while (imagePairEnum.hasMoreElements()) {
0378: imagePair = imagePairEnum.nextImagePair();
0379: JMLEqualsSet img = (JMLEqualsSet) imagePair.value;
0380: if (!img.intersection(rng).isEmpty()) {
0381: invImg = invImg.insert(imagePair.key);
0382: }
0383: }
0384: return invImg;
0385: }
0386:
0387: /** Tells whether this relation associates any range element to the
0388: * given domain element.
0389: * @see #domain()
0390: */
0391: /*@ public normal_behavior
0392: @ ensures \result == (elementImage(dv).int_size() > 0);
0393: @ ensures_redundantly dv == null ==> !\result;
0394: @*/
0395: public boolean isDefinedAt(JMLType dv) {
0396: return domain_.has(dv);
0397: }
0398:
0399: /** Tells whether this associates the given key to the given value.
0400: * @see #isDefinedAt
0401: * @see #has(JMLValueEqualsPair)
0402: */
0403: /*@ public normal_behavior
0404: @ ensures \result <==> domain().has(dv) && elementImage(dv).has(rv);
0405: @ ensures_redundantly dv == null || rv == null ==> !\result;
0406: @*/
0407: public/*@ pure @*/boolean has(JMLType dv, Object rv) {
0408: return domain_.has(dv) && elementImage(dv).has(rv);
0409: }
0410:
0411: /** Tells whether this associates the given key to the given value.
0412: * @see #isDefinedAt
0413: * @see #has(JMLType, Object)
0414: */
0415: /*@ public normal_behavior
0416: @ requires pair != null;
0417: @ ensures \result <==> has(pair.key, pair.value);
0418: @*/
0419: public/*@ pure @*/boolean has(
0420: /*@ non_null @*/JMLValueEqualsPair pair) {
0421: return has(pair.key, pair.value);
0422: }
0423:
0424: /** Tells whether this associates the given key to the given value.
0425: * @see #isDefinedAt
0426: * @see #has(JMLValueEqualsPair)
0427: */
0428: /*@ also
0429: @ public normal_behavior
0430: @ ensures \result <==>
0431: @ obj != null
0432: @ && obj instanceof JMLValueEqualsPair
0433: @ && has((JMLValueEqualsPair) obj);
0434: @*/
0435: public/*@ pure @*/boolean has(Object obj) {
0436: return obj != null && obj instanceof JMLValueEqualsPair
0437: && has((JMLValueEqualsPair) obj);
0438: }
0439:
0440: /** Tells whether the relation is empty.
0441: * @see #int_size()
0442: */
0443: /*@ public normal_behavior
0444: @ ensures \result == (theRelation.int_size() == 0);
0445: @*/
0446: public boolean isEmpty() {
0447: return size_ == 0;
0448: }
0449:
0450: /** Return a clone of this object.
0451: */
0452: /*@ also
0453: @ public normal_behavior
0454: @ ensures \result instanceof JMLValueToEqualsRelation
0455: @ && ((JMLValueToEqualsRelation)\result)
0456: @ .theRelation.equals(this.theRelation);
0457: @*/
0458: public Object clone() {
0459: return new JMLValueToEqualsRelation(imagePairSet_, domain_,
0460: size_);
0461: }
0462:
0463: /** Test whether this object's value is equal to the given argument.
0464: */
0465: /*@ also
0466: @ public normal_behavior
0467: @ requires obj != null && obj instanceof JMLValueToEqualsRelation;
0468: @ ensures \result ==
0469: @ this.theRelation.equals(
0470: @ ((JMLValueToEqualsRelation)obj).theRelation);
0471: @ also
0472: @ public normal_behavior
0473: @ requires obj == null
0474: @ || !(obj instanceof JMLValueToEqualsRelation);
0475: @ ensures !\result;
0476: @*/
0477: public boolean equals(Object obj) {
0478: if (obj == null || !(obj instanceof JMLValueToEqualsRelation)) {
0479: return false;
0480: }
0481:
0482: JMLValueToEqualsRelation rel = (JMLValueToEqualsRelation) obj;
0483:
0484: if (size_ != rel.int_size()) {
0485: return false;
0486: }
0487:
0488: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0489: .imagePairs();
0490: JMLValueValuePair imagePair;
0491: JMLEqualsSet img;
0492: while (imagePairEnum.hasMoreElements()) {
0493: imagePair = imagePairEnum.nextImagePair();
0494: img = (JMLEqualsSet) imagePair.value;
0495: if (!img.equals(rel.elementImage(imagePair.key))) {
0496: return false;
0497: }
0498: }
0499: return true;
0500: }
0501:
0502: /** Return a hash code for this object.
0503: */
0504: public int hashCode() {
0505: return imagePairSet_.hashCode();
0506: }
0507:
0508: /** Returns a set containing the domain of this relation.
0509: * @see #domainElements()
0510: * @see #associations()
0511: * @see #isDefinedAt
0512: * @see #image
0513: * @see #range()
0514: * @see #inverse()
0515: */
0516: /*@ public normal_behavior
0517: @ ensures (\forall JMLType dv; ;
0518: @ \result.has(dv) == isDefinedAt(dv));
0519: @*/
0520: public/*@ non_null @*/JMLValueSet domain() {
0521: return domain_;
0522: }
0523:
0524: /** Returns a set containing the range of this relation.
0525: * @see #rangeElements()
0526: * @see #associations()
0527: * @see #inverseElementImage
0528: * @see #domain()
0529: * @see #inverse()
0530: */
0531: /*@ public normal_behavior
0532: @ ensures (\forall Object rv; ;
0533: @ \result.has(rv)
0534: @ == (\exists JMLType dv; ;
0535: @ elementImage(dv).has(rv))
0536: @ );
0537: @*/
0538: public/*@ non_null @*/JMLEqualsSet range() {
0539: JMLEqualsSet rangeSet = new JMLEqualsSet();
0540:
0541: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0542: .imagePairs();
0543: JMLValueValuePair imagePair;
0544: JMLEqualsSet img;
0545: while (imagePairEnum.hasMoreElements()) {
0546: imagePair = imagePairEnum.nextImagePair();
0547: img = (JMLEqualsSet) imagePair.value;
0548: rangeSet = rangeSet.union(img);
0549: }
0550: return rangeSet;
0551: }
0552:
0553: private static final String TOO_BIG_TO_INSERT = "Cannot insert into a Relation with Integer.MAX_VALUE elements.";
0554:
0555: /** Return a relation that is just like this relation, except that
0556: * it also associates the given domain element to the given range
0557: * element.
0558: * @see #insert
0559: */
0560: /*@ public normal_behavior
0561: @ requires dv != null && rv != null;
0562: @ requires int_size() < Integer.MAX_VALUE || elementImage(dv).has(rv);
0563: @ ensures \result.theRelation.equals(
0564: @ this.theRelation.insert(new JMLValueEqualsPair(dv, rv)));
0565: @*/
0566: public/*@ pure @*//*@ non_null @*/
0567: JMLValueToEqualsRelation add(/*@ non_null @*/JMLType dv,
0568: /*@ non_null @*/Object rv) throws NullPointerException,
0569: IllegalStateException {
0570: if (rv == null) {
0571: throw new NullPointerException();
0572: }
0573:
0574: JMLValueSet newImagePairSet;
0575: JMLValueSet newDom;
0576: int newSize;
0577: JMLEqualsSet img;
0578:
0579: if (!domain_.has(dv)) {
0580: if (size_ == Integer.MAX_VALUE) {
0581: throw new IllegalStateException(TOO_BIG_TO_INSERT);
0582: }
0583: newDom = domain_.insert(dv);
0584: newSize = size_ + 1;
0585: img = new JMLEqualsSet(rv);
0586: newImagePairSet = imagePairSet_
0587: .insert(new JMLValueValuePair(dv, img));
0588: } else {
0589: newImagePairSet = new JMLValueSet();
0590: newDom = domain_;
0591: newSize = 0;
0592:
0593: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0594: .imagePairs();
0595: JMLValueValuePair imagePair;
0596: while (imagePairEnum.hasMoreElements()) {
0597: imagePair = imagePairEnum.nextImagePair();
0598: img = (JMLEqualsSet) imagePair.value;
0599: if (imagePair.keyEquals(dv)) {
0600: img = img.insert(rv);
0601: }
0602: int size_inc = img.int_size();
0603: if (newSize <= Integer.MAX_VALUE - size_inc) {
0604: newSize = newSize + size_inc;
0605: } else {
0606: throw new IllegalStateException(TOO_BIG_TO_INSERT);
0607: }
0608: newImagePairSet = newImagePairSet
0609: .insert(new JMLValueValuePair(imagePair.key,
0610: img));
0611: }
0612: }
0613: return new JMLValueToEqualsRelation(newImagePairSet, newDom,
0614: newSize);
0615: }
0616:
0617: /** Return a relation that is just like this relation, except that
0618: * it also includes the association described by the given pair.
0619: * @see #add
0620: */
0621: /*@ public normal_behavior
0622: @ requires pair != null;
0623: @ requires int_size() < Integer.MAX_VALUE
0624: @ || elementImage(pair.key).has(pair.value);
0625: @ ensures \result.theRelation.equals(this.theRelation.insert(pair));
0626: @*/
0627: public/*@ non_null @*/
0628: JMLValueToEqualsRelation insert(/*@ non_null @*/
0629: JMLValueEqualsPair pair) throws IllegalStateException {
0630: return add(pair.key, pair.value);
0631: }
0632:
0633: /** Return a relation that is just like this relation, except that
0634: * it does not contain any association with the given domain element.
0635: * @see #remove(JMLValueEqualsPair)
0636: * @see #removeFromDomain
0637: */
0638: /*@ public normal_behavior
0639: @ ensures \result != null
0640: @ && (\forall JMLType val; domain().has(val);
0641: @ (\forall Object r; r != null;
0642: @ (elementImage(val).has(r)
0643: @ <==> \result.theRelation
0644: @ .has(new JMLValueEqualsPair(val,r))
0645: @ && !val.equals(dv))));
0646: @ implies_that
0647: @ public normal_behavior
0648: @ requires dv == null;
0649: @ ensures \result != null && \result.equals(this);
0650: @*/
0651: public/*@ non_null @*/
0652: JMLValueToEqualsRelation removeFromDomain(JMLType dv) {
0653: if (!domain_.has(dv)) {
0654: return (this );
0655: }
0656:
0657: JMLValueSet newImagePairSet = new JMLValueSet();
0658: JMLValueSet newDom = domain_.remove(dv);
0659: int newSize = 0;
0660:
0661: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0662: .imagePairs();
0663: JMLValueValuePair imagePair;
0664: while (imagePairEnum.hasMoreElements()) {
0665: imagePair = imagePairEnum.nextImagePair();
0666: if (!imagePair.keyEquals(dv)) {
0667: newImagePairSet = newImagePairSet.insert(imagePair);
0668: JMLEqualsSet img = (JMLEqualsSet) imagePair.value;
0669: newSize = newSize + img.int_size();
0670: }
0671: }
0672: return new JMLValueToEqualsRelation(newImagePairSet, newDom,
0673: newSize);
0674: }
0675:
0676: /** Return a relation that is just like this relation, except that
0677: * it does not contain the association, if any, between the given
0678: * domain and range elements.
0679: * @see #removeFromDomain
0680: * @see #remove(JMLType, Object)
0681: * @see #remove(JMLValueEqualsPair)
0682: */
0683: /*@ public normal_behavior
0684: @ requires dv != null && rv != null;
0685: @ ensures \result.theRelation.equals(
0686: @ theRelation.remove(new JMLValueEqualsPair(dv, rv)));
0687: @ also
0688: @ requires dv == null || rv == null;
0689: @ ensures \result != null && \result.equals(this);
0690: @*/
0691: public/*@ non_null @*/
0692: JMLValueToEqualsRelation remove(JMLType dv, Object rv) {
0693: if (!domain_.has(dv)) {
0694: return (this );
0695: }
0696:
0697: JMLValueSet newImagePairSet = new JMLValueSet();
0698: JMLValueSet newDom = domain_;
0699: int newSize = 0;
0700:
0701: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0702: .imagePairs();
0703: JMLValueValuePair imagePair;
0704: JMLEqualsSet img;
0705: while (imagePairEnum.hasMoreElements()) {
0706: imagePair = imagePairEnum.nextImagePair();
0707: img = (JMLEqualsSet) imagePair.value;
0708: int imgSize = img.int_size();
0709: if (imagePair.keyEquals(dv)) {
0710: img = img.remove(rv);
0711: imgSize = img.int_size();
0712: if (imgSize > 0) {
0713: newImagePairSet = newImagePairSet
0714: .insert(new JMLValueValuePair(dv, img));
0715: newSize = newSize + imgSize;
0716: } else {
0717: newDom = newDom.remove(dv);
0718: }
0719: } else {
0720: newImagePairSet = newImagePairSet.insert(imagePair);
0721: newSize = newSize + imgSize;
0722: }
0723: }
0724: return new JMLValueToEqualsRelation(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(JMLType, Object)
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: JMLValueToEqualsRelation remove(/*@ non_null @*/
0739: JMLValueEqualsPair 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(JMLObjectToValueRelation)
0749: */
0750: /*@ public normal_behavior
0751: @ requires othRel != null;
0752: @ ensures (\forall JMLValueEqualsPair pair; ;
0753: @ \result.theRelation.has(pair)
0754: @ == (\exists JMLType val;
0755: @ othRel.elementImage(pair.key).has(val);
0756: @ this.elementImage(val).has(pair.value)
0757: @ )
0758: @ );
0759: @*/
0760: public/*@ non_null @*/
0761: JMLValueToEqualsRelation compose(
0762: /*@ non_null @*/JMLValueToValueRelation othRel) {
0763: JMLValueSet newImagePairSet = new JMLValueSet();
0764: JMLValueSet newDom = new JMLValueSet();
0765: int newSize = 0;
0766:
0767: JMLValueToValueRelationImageEnumerator imagePairEnum = othRel
0768: .imagePairs();
0769: JMLValueValuePair imagePair;
0770: JMLValueSet img1;
0771: JMLEqualsSet img2;
0772: int imgSize;
0773: while (imagePairEnum.hasMoreElements()) {
0774: imagePair = imagePairEnum.nextImagePair();
0775: img1 = (JMLValueSet) 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 JMLValueToEqualsRelation(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(JMLValueToValueRelation)
0796: */
0797: /*@ public normal_behavior
0798: @ requires othRel != null;
0799: @ ensures (\forall JMLValueEqualsPair pair; ;
0800: @ \result.theRelation.has(pair)
0801: @ == (\exists JMLType val;
0802: @ othRel.elementImage(pair.key).has(val);
0803: @ this.elementImage(val).has(pair.value)
0804: @ )
0805: @ );
0806: @*/
0807: public/*@ non_null @*/
0808: JMLObjectToEqualsRelation compose(
0809: /*@ non_null @*/JMLObjectToValueRelation othRel) {
0810: JMLValueSet newImagePairSet = new JMLValueSet();
0811: JMLObjectSet newDom = new JMLObjectSet();
0812: int newSize = 0;
0813:
0814: JMLObjectToValueRelationImageEnumerator imagePairEnum = othRel
0815: .imagePairs();
0816: JMLObjectValuePair imagePair;
0817: JMLValueSet img1;
0818: JMLEqualsSet img2;
0819: int imgSize;
0820: while (imagePairEnum.hasMoreElements()) {
0821: imagePair = imagePairEnum.nextImagePair();
0822: img1 = (JMLValueSet) 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 JMLObjectToEqualsRelation(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: JMLValueToEqualsRelation union(
0851: /*@ non_null @*/JMLValueToEqualsRelation othRel)
0852: throws IllegalStateException {
0853: JMLValueSet newImagePairSet = new JMLValueSet();
0854: JMLValueSet newDom = domain_;
0855: int newSize = 0;
0856:
0857: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0858: .imagePairs();
0859: JMLValueValuePair imagePair;
0860: JMLEqualsSet img;
0861: while (imagePairEnum.hasMoreElements()) {
0862: imagePair = imagePairEnum.nextImagePair();
0863: img = (JMLEqualsSet) imagePair.value;
0864: img = img.union(othRel.elementImage(imagePair.key));
0865: newImagePairSet = newImagePairSet
0866: .insert(new JMLValueValuePair(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: JMLValueSet 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 = (JMLEqualsSet) 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 JMLValueToEqualsRelation(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: JMLValueToEqualsRelation intersection(
0909: /*@ non_null @*/JMLValueToEqualsRelation othRel) {
0910: JMLValueSet newImagePairSet = new JMLValueSet();
0911: JMLValueSet newDom = new JMLValueSet();
0912: int newSize = 0;
0913:
0914: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0915: .imagePairs();
0916: JMLValueValuePair imagePair;
0917: JMLEqualsSet img;
0918: while (imagePairEnum.hasMoreElements()) {
0919: imagePair = imagePairEnum.nextImagePair();
0920: img = (JMLEqualsSet) imagePair.value;
0921: img = img.intersection(othRel.elementImage(imagePair.key));
0922: if (!img.isEmpty()) {
0923: newImagePairSet = newImagePairSet
0924: .insert(new JMLValueValuePair(imagePair.key,
0925: img));
0926: newDom = newDom.insert(imagePair.key);
0927: newSize = newSize + img.int_size();
0928: }
0929: }
0930: return new JMLValueToEqualsRelation(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: JMLValueToEqualsRelation difference(
0947: /*@ non_null @*/JMLValueToEqualsRelation othRel) {
0948: JMLValueSet newImagePairSet = new JMLValueSet();
0949: JMLValueSet newDom = new JMLValueSet();
0950: int newSize = 0;
0951:
0952: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0953: .imagePairs();
0954: JMLValueValuePair imagePair;
0955: JMLEqualsSet img;
0956: while (imagePairEnum.hasMoreElements()) {
0957: imagePair = imagePairEnum.nextImagePair();
0958: img = (JMLEqualsSet) imagePair.value;
0959: img = img.difference(othRel.elementImage(imagePair.key));
0960: if (!img.isEmpty()) {
0961: newImagePairSet = newImagePairSet
0962: .insert(new JMLValueValuePair(imagePair.key,
0963: img));
0964: newDom = newDom.insert(imagePair.key);
0965: newSize = newSize + img.int_size();
0966: }
0967: }
0968: return new JMLValueToEqualsRelation(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 JMLValueEqualsPair 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: JMLValueToEqualsRelation restrictDomainTo(
0985: /*@ non_null @*/JMLValueSet dom) {
0986: JMLValueSet newImagePairSet = new JMLValueSet();
0987: JMLValueSet newDom = domain_.intersection(dom);
0988: int newSize = 0;
0989:
0990: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
0991: .imagePairs();
0992: JMLValueValuePair imagePair;
0993: JMLEqualsSet img;
0994: while (imagePairEnum.hasMoreElements()) {
0995: imagePair = imagePairEnum.nextImagePair();
0996: if (newDom.has(imagePair.key)) {
0997: newImagePairSet = newImagePairSet.insert(imagePair);
0998: img = (JMLEqualsSet) imagePair.value;
0999: newSize = newSize + img.int_size();
1000: }
1001: }
1002: return new JMLValueToEqualsRelation(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 JMLValueEqualsPair 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: JMLValueToEqualsRelation restrictRangeTo(
1020: /*@ non_null @*/JMLEqualsSet rng) {
1021: JMLValueSet newImagePairSet = new JMLValueSet();
1022: JMLValueSet newDom = new JMLValueSet();
1023: int newSize = 0;
1024:
1025: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
1026: .imagePairs();
1027: JMLValueValuePair imagePair;
1028: JMLEqualsSet img;
1029: while (imagePairEnum.hasMoreElements()) {
1030: imagePair = imagePairEnum.nextImagePair();
1031: img = ((JMLEqualsSet) imagePair.value).intersection(rng);
1032: if (!img.isEmpty()) {
1033: newImagePairSet = newImagePairSet
1034: .insert(new JMLValueValuePair(imagePair.key,
1035: img));
1036: newDom = newDom.insert(imagePair.key);
1037: newSize = newSize + img.int_size();
1038: }
1039: }
1040: return new JMLValueToEqualsRelation(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 JMLValueToEqualsRelationEnumerator(this));
1064: @*/
1065: public/*@ non_null @*/
1066: JMLValueToEqualsRelationEnumerator associations() {
1067: return new JMLValueToEqualsRelationEnumerator(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: JMLValueToEqualsRelationEnumerator 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 JMLValueEqualsPair
1107: @ && this.isDefinedAt(((JMLValueEqualsPair)pv).key)
1108: @ && this.elementImage(((JMLValueEqualsPair)pv).key)
1109: @ .has(((JMLValueEqualsPair)pv).value));
1110: @
1111: @*/
1112: public/*@ non_null @*/JMLValueSet toSet() {
1113: JMLValueToEqualsRelationEnumerator pairEnum = this
1114: .associations();
1115: JMLValueSet ret = new JMLValueSet();
1116: while (pairEnum.hasMoreElements()) {
1117: JMLValueEqualsPair 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: JMLValueToEqualsRelationEnumerator pairEnum = this
1132: .associations();
1133: JMLValueBag ret = new JMLValueBag();
1134: while (pairEnum.hasMoreElements()) {
1135: JMLValueEqualsPair 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 JMLValueEqualsPair p;;
1148: @ \result.count(p) == 1 <==> this.has(p));
1149: @*/
1150: public/*@ non_null @*/JMLValueSequence toSequence() {
1151: JMLValueToEqualsRelationEnumerator pairEnum = this
1152: .associations();
1153: JMLValueSequence ret = new JMLValueSequence();
1154: while (pairEnum.hasMoreElements()) {
1155: JMLValueEqualsPair 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 JMLType dv; domain().has(dv);
1168: @ \result.has(
1169: @ new JMLValueValuePair(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 JMLType dv; domain().has(dv);
1184: @ \result.abstractValue().has(
1185: @ new JMLValueValuePair(dv, elementImage(dv))));
1186: @*/
1187: public/*@ non_null @*/
1188: JMLValueToEqualsRelationImageEnumerator imagePairs() {
1189: return new JMLValueToEqualsRelationImageEnumerator(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 @*/JMLValueSetEnumerator 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 @*/JMLEqualsSetEnumerator 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 JMLValueToEqualsMap
1234: */
1235: /*@ public normal_behavior
1236: @ ensures (\forall JMLType 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 @*/JMLValueToEqualsMap toFunction() {
1242: JMLValueSet 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: JMLValueToEqualsRelationImageEnumerator imagePairEnum = this
1250: .imagePairs();
1251: newImagePairSet = new JMLValueSet();
1252: JMLValueValuePair imagePair;
1253: JMLEqualsSet img;
1254: while (imagePairEnum.hasMoreElements()) {
1255: imagePair = imagePairEnum.nextImagePair();
1256: img = (JMLEqualsSet) imagePair.value;
1257: Enumeration imgEnum = img.elements();
1258: Object o = imgEnum.nextElement();
1259: if (o == null) {
1260: img = new JMLEqualsSet(null);
1261: } else {
1262: Object rv = (Object) o;
1263: img = new JMLEqualsSet(rv);
1264: }
1265: newImagePairSet = newImagePairSet
1266: .insert(new JMLValueValuePair(imagePair.key,
1267: img));
1268: }
1269: }
1270: return new JMLValueToEqualsMap(newImagePairSet, newDom, newSize);
1271: }
1272: }
|