0001: // @(#)$Id: JMLEqualsToObjectRelation.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: * Object}. The first type, <kbd>Object</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.1.1.1 $
0046: * @author Gary T. Leavens
0047: * @author Clyde Ruby
0048: * @see JMLCollection
0049: * @see JMLType
0050: * @see JMLEqualsToObjectMap
0051: * @see JMLEqualsToObjectRelationEnumerator
0052: * @see JMLEqualsToObjectRelationImageEnumerator
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 JMLEqualsToObjectRelation 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 JMLEqualsObjectPair
0072: @ && ((JMLEqualsObjectPair)obj).key != null
0073: @ && ((JMLEqualsObjectPair)obj).value != null);
0074: @ public invariant_redundantly
0075: @ (* Every element of 'theRelation'is a JMLEqualsObjectPair
0076: @ whose key and value are not null *);
0077: @*/
0078:
0079: //@ public invariant elementType == \type(JMLEqualsObjectPair);
0080: //@ public invariant !containsNull;
0081: /** The set of elements in the domain of this relation.
0082: */
0083: protected final/*@ non_null @*/JMLEqualsSet domain_;
0084: //@ in theRelation;
0085:
0086: /** The set representing the image pairs in the relation. The
0087: * elements of this set are JMLEqualsValuePairs, 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 JMLObjectSet 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 JMLEqualsValuePair(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 JMLEqualsToObjectRelation() {
0124: domain_ = new JMLEqualsSet();
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, Object)
0132: * @see #JMLEqualsToObjectRelation(JMLEqualsObjectPair)
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 JMLEqualsToObjectRelation(/*@ non_null @*/Object dv,
0142: /*@ non_null @*/Object rv) {
0143: size_ = 1;
0144: domain_ = new JMLEqualsSet(dv);
0145: JMLObjectSet img = new JMLObjectSet(rv);
0146: imagePairSet_ = new JMLValueSet(new JMLEqualsValuePair(dv, img));
0147: }
0148:
0149: /** Initialize this to be a relation containing a single association
0150: * given by the pair.
0151: * @see #singleton(JMLEqualsObjectPair)
0152: * @see #JMLEqualsToObjectRelation(Object, 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 JMLEqualsToObjectRelation(/*@ non_null @*/
0160: JMLEqualsObjectPair 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 JMLEqualsToObjectRelation(
0177: /*@ non_null @*/JMLValueSet ipset,
0178: /*@ non_null @*/JMLEqualsSet dom, int sz) {
0179: domain_ = dom;
0180: imagePairSet_ = ipset;
0181: size_ = sz;
0182: }
0183:
0184: //**************************** Static methods ****************************
0185:
0186: /** The empty JMLEqualsToObjectRelation.
0187: * @see #JMLEqualsToObjectRelation()
0188: */
0189: public static final/*@ non_null @*/JMLEqualsToObjectRelation EMPTY = new JMLEqualsToObjectRelation();
0190:
0191: /** Return the singleton relation containing the given association.
0192: * @see #singleton(JMLEqualsObjectPair)
0193: * @see #JMLEqualsToObjectRelation(Object, Object)
0194: */
0195: /*@ public normal_behavior
0196: @ requires dv != null && rv != null;
0197: @ ensures \result != null
0198: @ && \result.equals(new JMLEqualsToObjectRelation(dv, rv));
0199: @*/
0200: public static/*@ pure @*//*@ non_null @*/
0201: JMLEqualsToObjectRelation singleton(/*@ non_null @*/Object dv,
0202: /*@ non_null @*/Object rv) {
0203: return new JMLEqualsToObjectRelation(dv, rv);
0204: }
0205:
0206: /** Return the singleton relation containing the association
0207: * described by the given pair.
0208: * @see #singleton(Object, Object)
0209: * @see #JMLEqualsToObjectRelation(JMLEqualsObjectPair)
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: JMLEqualsToObjectRelation singleton(
0218: /*@ non_null @*/JMLEqualsObjectPair pair) {
0219: return singleton(pair.key, pair.value);
0220: }
0221:
0222: //**************************** Observers **********************************
0223:
0224: /** Tells whether this relation is a function.
0225: * @see JMLEqualsToObjectMap
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 JMLEqualsToObjectMap#apply
0239: */
0240: /*@ public normal_behavior
0241: @ ensures (\forall JMLEqualsObjectPair pair;
0242: @ theRelation.has(pair);
0243: @ pair.keyEquals(dv) ==> \result.has(pair.value));
0244: @ ensures (\forall Object o; \result.has(o);
0245: @ (\exists JMLEqualsObjectPair 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: JMLObjectSet elementImage(Object dv) {
0255: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0256: .imagePairs();
0257: JMLEqualsValuePair imagePair;
0258: while (imagePairEnum.hasMoreElements()) {
0259: imagePair = imagePairEnum.nextImagePair();
0260: if (imagePair.keyEquals(dv)) {
0261: JMLObjectSet res = (JMLObjectSet) imagePair.value;
0262: return res;
0263: }
0264: }
0265: return new JMLObjectSet();
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 JMLEqualsToObjectMap#apply
0273: */
0274: /*@ public normal_behavior
0275: @ requires dom != null;
0276: @ ensures (\forall Object o; \result.has(o)
0277: @ <==> (\exists JMLEqualsObjectPair pair;
0278: @ theRelation.has(pair);
0279: @ dom.has(pair.key) && pair.valueEquals(o)));
0280: @ ensures_redundantly
0281: @ (\forall JMLEqualsObjectPair 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: JMLObjectSet image(/*@ non_null @*/JMLEqualsSet dom) {
0290: JMLObjectSet img = new JMLObjectSet();
0291: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0292: .imagePairs();
0293: JMLEqualsValuePair imagePair;
0294: //@ loop_invariant !img.containsNull;
0295: while (imagePairEnum.hasMoreElements()) {
0296: imagePair = imagePairEnum.nextImagePair();
0297: if (dom.has(imagePair.key)) {
0298: JMLObjectSet ipv = (JMLObjectSet) 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 JMLObjectEqualsPair pair; ;
0313: @ \result.theRelation.has(pair)
0314: @ == elementImage(pair.value).has(pair.key));
0315: @*/
0316: public/*@ non_null @*/JMLObjectToEqualsRelation inverse() {
0317: JMLObjectToEqualsRelation invRel = new JMLObjectToEqualsRelation();
0318: JMLEqualsToObjectRelationEnumerator assocEnum = this
0319: .associations();
0320: JMLEqualsObjectPair 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: JMLEqualsSet inverseElementImage(Object rv) {
0342: JMLEqualsSet invImg = new JMLEqualsSet();
0343: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0344: .imagePairs();
0345: JMLEqualsValuePair imagePair;
0346: //@ loop_invariant !invImg.containsNull;
0347: while (imagePairEnum.hasMoreElements()) {
0348: imagePair = imagePairEnum.nextImagePair();
0349: JMLObjectSet img = (JMLObjectSet) 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: JMLEqualsSet inverseImage(/*@ non_null @*/JMLObjectSet rng) {
0372: JMLEqualsSet invImg = new JMLEqualsSet();
0373: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0374: .imagePairs();
0375: JMLEqualsValuePair imagePair;
0376: //@ loop_invariant !invImg.containsNull;
0377: while (imagePairEnum.hasMoreElements()) {
0378: imagePair = imagePairEnum.nextImagePair();
0379: JMLObjectSet img = (JMLObjectSet) 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(Object 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(JMLEqualsObjectPair)
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(Object 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(Object, 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 @*/JMLEqualsObjectPair 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(JMLEqualsObjectPair)
0427: */
0428: /*@ also
0429: @ public normal_behavior
0430: @ ensures \result <==>
0431: @ obj != null
0432: @ && obj instanceof JMLEqualsObjectPair
0433: @ && has((JMLEqualsObjectPair) obj);
0434: @*/
0435: public/*@ pure @*/boolean has(Object obj) {
0436: return obj != null && obj instanceof JMLEqualsObjectPair
0437: && has((JMLEqualsObjectPair) 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 JMLEqualsToObjectRelation
0455: @ && ((JMLEqualsToObjectRelation)\result)
0456: @ .theRelation.equals(this.theRelation);
0457: @*/
0458: public Object clone() {
0459: return new JMLEqualsToObjectRelation(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 JMLEqualsToObjectRelation;
0468: @ ensures \result ==
0469: @ this.theRelation.equals(
0470: @ ((JMLEqualsToObjectRelation)obj).theRelation);
0471: @ also
0472: @ public normal_behavior
0473: @ requires obj == null
0474: @ || !(obj instanceof JMLEqualsToObjectRelation);
0475: @ ensures !\result;
0476: @*/
0477: public boolean equals(Object obj) {
0478: if (obj == null || !(obj instanceof JMLEqualsToObjectRelation)) {
0479: return false;
0480: }
0481:
0482: JMLEqualsToObjectRelation rel = (JMLEqualsToObjectRelation) obj;
0483:
0484: if (size_ != rel.int_size()) {
0485: return false;
0486: }
0487:
0488: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0489: .imagePairs();
0490: JMLEqualsValuePair imagePair;
0491: JMLObjectSet img;
0492: while (imagePairEnum.hasMoreElements()) {
0493: imagePair = imagePairEnum.nextImagePair();
0494: img = (JMLObjectSet) 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 Object dv; ;
0518: @ \result.has(dv) == isDefinedAt(dv));
0519: @*/
0520: public/*@ non_null @*/JMLEqualsSet 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 Object dv; ;
0535: @ elementImage(dv).has(rv))
0536: @ );
0537: @*/
0538: public/*@ non_null @*/JMLObjectSet range() {
0539: JMLObjectSet rangeSet = new JMLObjectSet();
0540:
0541: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0542: .imagePairs();
0543: JMLEqualsValuePair imagePair;
0544: JMLObjectSet img;
0545: while (imagePairEnum.hasMoreElements()) {
0546: imagePair = imagePairEnum.nextImagePair();
0547: img = (JMLObjectSet) 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 JMLEqualsObjectPair(dv, rv)));
0565: @*/
0566: public/*@ pure @*//*@ non_null @*/
0567: JMLEqualsToObjectRelation add(/*@ non_null @*/Object dv,
0568: /*@ non_null @*/Object rv) throws NullPointerException,
0569: IllegalStateException {
0570: if (rv == null) {
0571: throw new NullPointerException();
0572: }
0573:
0574: JMLValueSet newImagePairSet;
0575: JMLEqualsSet newDom;
0576: int newSize;
0577: JMLObjectSet 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 JMLObjectSet(rv);
0586: newImagePairSet = imagePairSet_
0587: .insert(new JMLEqualsValuePair(dv, img));
0588: } else {
0589: newImagePairSet = new JMLValueSet();
0590: newDom = domain_;
0591: newSize = 0;
0592:
0593: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0594: .imagePairs();
0595: JMLEqualsValuePair imagePair;
0596: while (imagePairEnum.hasMoreElements()) {
0597: imagePair = imagePairEnum.nextImagePair();
0598: img = (JMLObjectSet) 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 JMLEqualsValuePair(imagePair.key,
0610: img));
0611: }
0612: }
0613: return new JMLEqualsToObjectRelation(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: JMLEqualsToObjectRelation insert(/*@ non_null @*/
0629: JMLEqualsObjectPair 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(JMLEqualsObjectPair)
0636: * @see #removeFromDomain
0637: */
0638: /*@ public normal_behavior
0639: @ ensures \result != null
0640: @ && (\forall Object val; domain().has(val);
0641: @ (\forall Object r; r != null;
0642: @ (elementImage(val).has(r)
0643: @ <==> \result.theRelation
0644: @ .has(new JMLEqualsObjectPair(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: JMLEqualsToObjectRelation removeFromDomain(Object dv) {
0653: if (!domain_.has(dv)) {
0654: return (this );
0655: }
0656:
0657: JMLValueSet newImagePairSet = new JMLValueSet();
0658: JMLEqualsSet newDom = domain_.remove(dv);
0659: int newSize = 0;
0660:
0661: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0662: .imagePairs();
0663: JMLEqualsValuePair imagePair;
0664: while (imagePairEnum.hasMoreElements()) {
0665: imagePair = imagePairEnum.nextImagePair();
0666: if (!imagePair.keyEquals(dv)) {
0667: newImagePairSet = newImagePairSet.insert(imagePair);
0668: JMLObjectSet img = (JMLObjectSet) imagePair.value;
0669: newSize = newSize + img.int_size();
0670: }
0671: }
0672: return new JMLEqualsToObjectRelation(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(Object, Object)
0681: * @see #remove(JMLEqualsObjectPair)
0682: */
0683: /*@ public normal_behavior
0684: @ requires dv != null && rv != null;
0685: @ ensures \result.theRelation.equals(
0686: @ theRelation.remove(new JMLEqualsObjectPair(dv, rv)));
0687: @ also
0688: @ requires dv == null || rv == null;
0689: @ ensures \result != null && \result.equals(this);
0690: @*/
0691: public/*@ non_null @*/
0692: JMLEqualsToObjectRelation remove(Object dv, Object rv) {
0693: if (!domain_.has(dv)) {
0694: return (this );
0695: }
0696:
0697: JMLValueSet newImagePairSet = new JMLValueSet();
0698: JMLEqualsSet newDom = domain_;
0699: int newSize = 0;
0700:
0701: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0702: .imagePairs();
0703: JMLEqualsValuePair imagePair;
0704: JMLObjectSet img;
0705: while (imagePairEnum.hasMoreElements()) {
0706: imagePair = imagePairEnum.nextImagePair();
0707: img = (JMLObjectSet) 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 JMLEqualsValuePair(dv, img));
0715: newSize = newSize + imgSize;
0716: } else {
0717: //@ assert imgSize == 0;
0718: newDom = newDom.remove(dv);
0719: }
0720: } else {
0721: newImagePairSet = newImagePairSet.insert(imagePair);
0722: newSize = newSize + imgSize;
0723: }
0724: }
0725: return new JMLEqualsToObjectRelation(newImagePairSet, newDom,
0726: newSize);
0727: }
0728:
0729: /** Return a relation that is just like this relation, except that
0730: * it does not contain association described by the given pair.
0731: * @see #remove(Object, Object)
0732: * @see #removeFromDomain
0733: */
0734: /*@ public normal_behavior
0735: @ requires pair != null;
0736: @ ensures \result.theRelation.equals(this.theRelation.remove(pair));
0737: @*/
0738: public/*@ non_null @*/
0739: JMLEqualsToObjectRelation remove(/*@ non_null @*/
0740: JMLEqualsObjectPair pair) {
0741: return remove(pair.key, pair.value);
0742: }
0743:
0744: /** Return a relation that is the composition of the given
0745: * relation and this relation. The composition is done in the
0746: * "usual" order, so that if the given relation relates x to y,
0747: * and this relation relates y to z, then the result relates x to
0748: * z.
0749: * @see #compose(JMLObjectToEqualsRelation)
0750: */
0751: /*@ public normal_behavior
0752: @ requires othRel != null;
0753: @ ensures (\forall JMLValueObjectPair pair; ;
0754: @ \result.theRelation.has(pair)
0755: @ == (\exists Object val;
0756: @ othRel.elementImage(pair.key).has(val);
0757: @ this.elementImage(val).has(pair.value)
0758: @ )
0759: @ );
0760: @*/
0761: public/*@ non_null @*/
0762: JMLValueToObjectRelation compose(
0763: /*@ non_null @*/JMLValueToEqualsRelation othRel) {
0764: JMLValueSet newImagePairSet = new JMLValueSet();
0765: JMLValueSet newDom = new JMLValueSet();
0766: int newSize = 0;
0767:
0768: JMLValueToEqualsRelationImageEnumerator imagePairEnum = othRel
0769: .imagePairs();
0770: JMLValueValuePair imagePair;
0771: JMLEqualsSet img1;
0772: JMLObjectSet img2;
0773: int imgSize;
0774: while (imagePairEnum.hasMoreElements()) {
0775: imagePair = imagePairEnum.nextImagePair();
0776: img1 = (JMLEqualsSet) imagePair.value;
0777: img2 = this .image(img1);
0778: imgSize = img2.int_size();
0779: if (imgSize > 0) {
0780: newImagePairSet = newImagePairSet
0781: .insert(new JMLValueValuePair(imagePair.key,
0782: img2));
0783: newSize = newSize + imgSize;
0784: newDom = newDom.insert(imagePair.key);
0785: }
0786: }
0787: return new JMLValueToObjectRelation(newImagePairSet, newDom,
0788: newSize);
0789: }
0790:
0791: /** Return a relation that is the composition of the given
0792: * relation and this relation. The composition is done in the
0793: * "usual" order, so that if the given relation relates x to y,
0794: * and this relation relates y to z, then the result relates x to
0795: * z.
0796: * @see #compose(JMLValueToEqualsRelation)
0797: */
0798: /*@ public normal_behavior
0799: @ requires othRel != null;
0800: @ ensures (\forall JMLValueObjectPair pair; ;
0801: @ \result.theRelation.has(pair)
0802: @ == (\exists Object val;
0803: @ othRel.elementImage(pair.key).has(val);
0804: @ this.elementImage(val).has(pair.value)
0805: @ )
0806: @ );
0807: @*/
0808: public/*@ non_null @*/
0809: JMLObjectToObjectRelation compose(
0810: /*@ non_null @*/JMLObjectToEqualsRelation othRel) {
0811: JMLValueSet newImagePairSet = new JMLValueSet();
0812: JMLObjectSet newDom = new JMLObjectSet();
0813: int newSize = 0;
0814:
0815: JMLObjectToEqualsRelationImageEnumerator imagePairEnum = othRel
0816: .imagePairs();
0817: JMLObjectValuePair imagePair;
0818: JMLEqualsSet img1;
0819: JMLObjectSet img2;
0820: int imgSize;
0821: while (imagePairEnum.hasMoreElements()) {
0822: imagePair = imagePairEnum.nextImagePair();
0823: img1 = (JMLEqualsSet) imagePair.value;
0824: img2 = this .image(img1);
0825: imgSize = img2.int_size();
0826: if (imgSize > 0) {
0827: newImagePairSet = newImagePairSet
0828: .insert(new JMLObjectValuePair(imagePair.key,
0829: img2));
0830: newSize = newSize + imgSize;
0831: newDom = newDom.insert(imagePair.key);
0832: }
0833: }
0834: return new JMLObjectToObjectRelation(newImagePairSet, newDom,
0835: newSize);
0836: }
0837:
0838: /** Return a relation that union of the this and the given relation.
0839: * This is the union of the sets of associations.
0840: * @see #difference
0841: * @see #intersection
0842: */
0843: /*@ public normal_behavior
0844: @ requires othRel != null;
0845: @ requires int_size()
0846: @ < Integer.MAX_VALUE - othRel.difference(this).int_size();
0847: @ ensures \result.theRelation.equals(
0848: @ this.theRelation.union(othRel.theRelation));
0849: @*/
0850: public/*@ non_null @*/
0851: JMLEqualsToObjectRelation union(
0852: /*@ non_null @*/JMLEqualsToObjectRelation othRel)
0853: throws IllegalStateException {
0854: JMLValueSet newImagePairSet = new JMLValueSet();
0855: JMLEqualsSet newDom = domain_;
0856: int newSize = 0;
0857:
0858: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0859: .imagePairs();
0860: JMLEqualsValuePair imagePair;
0861: JMLObjectSet img;
0862: while (imagePairEnum.hasMoreElements()) {
0863: imagePair = imagePairEnum.nextImagePair();
0864: img = (JMLObjectSet) imagePair.value;
0865: img = img.union(othRel.elementImage(imagePair.key));
0866: newImagePairSet = newImagePairSet
0867: .insert(new JMLEqualsValuePair(imagePair.key, img));
0868: int size_inc = img.int_size();
0869: if (newSize <= Integer.MAX_VALUE - size_inc) {
0870: newSize = newSize + size_inc;
0871: } else {
0872: throw new IllegalStateException(TOO_BIG_TO_UNION);
0873: }
0874: }
0875: JMLEqualsSet diffDom = othRel.domain().difference(this .domain_);
0876: imagePairEnum = othRel.imagePairs();
0877: while (imagePairEnum.hasMoreElements()) {
0878: imagePair = imagePairEnum.nextImagePair();
0879: if (diffDom.has(imagePair.key)) {
0880: newImagePairSet = newImagePairSet.insert(imagePair);
0881: newDom = newDom.insert(imagePair.key);
0882: img = (JMLObjectSet) imagePair.value;
0883: int size_inc = img.int_size();
0884: if (newSize <= Integer.MAX_VALUE - size_inc) {
0885: newSize = newSize + size_inc;
0886: } else {
0887: throw new IllegalStateException(TOO_BIG_TO_UNION);
0888: }
0889: }
0890: }
0891: return new JMLEqualsToObjectRelation(newImagePairSet, newDom,
0892: newSize);
0893: }
0894:
0895: protected static final String TOO_BIG_TO_UNION = "Cannot make a union with more than Integer.MAX_VALUE elements.";
0896:
0897: /** Return a relation that is the intersection of this and the
0898: * given relation. This is the intersection of the sets of
0899: * associations.
0900: * @see #difference
0901: * @see #union
0902: */
0903: /*@ public normal_behavior
0904: @ requires othRel != null;
0905: @ ensures \result.theRelation.equals(
0906: @ this.theRelation.intersection(othRel.theRelation));
0907: @*/
0908: public/*@ non_null @*/
0909: JMLEqualsToObjectRelation intersection(
0910: /*@ non_null @*/JMLEqualsToObjectRelation othRel) {
0911: JMLValueSet newImagePairSet = new JMLValueSet();
0912: JMLEqualsSet newDom = new JMLEqualsSet();
0913: int newSize = 0;
0914:
0915: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0916: .imagePairs();
0917: JMLEqualsValuePair imagePair;
0918: JMLObjectSet img;
0919: while (imagePairEnum.hasMoreElements()) {
0920: imagePair = imagePairEnum.nextImagePair();
0921: img = (JMLObjectSet) imagePair.value;
0922: img = img.intersection(othRel.elementImage(imagePair.key));
0923: if (!img.isEmpty()) {
0924: newImagePairSet = newImagePairSet
0925: .insert(new JMLEqualsValuePair(imagePair.key,
0926: img));
0927: newDom = newDom.insert(imagePair.key);
0928: newSize = newSize + img.int_size();
0929: }
0930: }
0931: return new JMLEqualsToObjectRelation(newImagePairSet, newDom,
0932: newSize);
0933: }
0934:
0935: /** Return a relation that is the difference between this and the given
0936: * relation. This is the difference between the sets of
0937: * associations.
0938: * @see #difference
0939: * @see #intersection
0940: */
0941: /*@ public normal_behavior
0942: @ requires othRel != null;
0943: @ ensures \result.theRelation.equals(
0944: @ this.theRelation.difference(othRel.theRelation));
0945: @*/
0946: public/*@ non_null @*/
0947: JMLEqualsToObjectRelation difference(
0948: /*@ non_null @*/JMLEqualsToObjectRelation othRel) {
0949: JMLValueSet newImagePairSet = new JMLValueSet();
0950: JMLEqualsSet newDom = new JMLEqualsSet();
0951: int newSize = 0;
0952:
0953: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0954: .imagePairs();
0955: JMLEqualsValuePair imagePair;
0956: JMLObjectSet img;
0957: while (imagePairEnum.hasMoreElements()) {
0958: imagePair = imagePairEnum.nextImagePair();
0959: img = (JMLObjectSet) imagePair.value;
0960: img = img.difference(othRel.elementImage(imagePair.key));
0961: if (!img.isEmpty()) {
0962: newImagePairSet = newImagePairSet
0963: .insert(new JMLEqualsValuePair(imagePair.key,
0964: img));
0965: newDom = newDom.insert(imagePair.key);
0966: newSize = newSize + img.int_size();
0967: }
0968: }
0969: return new JMLEqualsToObjectRelation(newImagePairSet, newDom,
0970: newSize);
0971: }
0972:
0973: /** Return a relation that is like this relation except that its
0974: * domain is limited to just the elements of the given set.
0975: * @see #restrictRangeTo
0976: */
0977: /*@ public normal_behavior
0978: @ requires dom != null;
0979: @ ensures (\forall JMLEqualsObjectPair pair; pair != null;
0980: @ \result.theRelation.has(pair) == dom.has(pair.key)
0981: @ && elementImage(pair.key).has(pair.value)
0982: @ );
0983: @*/
0984: public/*@ non_null @*/
0985: JMLEqualsToObjectRelation restrictDomainTo(
0986: /*@ non_null @*/JMLEqualsSet dom) {
0987: JMLValueSet newImagePairSet = new JMLValueSet();
0988: JMLEqualsSet newDom = domain_.intersection(dom);
0989: int newSize = 0;
0990:
0991: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
0992: .imagePairs();
0993: JMLEqualsValuePair imagePair;
0994: JMLObjectSet img;
0995: while (imagePairEnum.hasMoreElements()) {
0996: imagePair = imagePairEnum.nextImagePair();
0997: if (newDom.has(imagePair.key)) {
0998: newImagePairSet = newImagePairSet.insert(imagePair);
0999: img = (JMLObjectSet) imagePair.value;
1000: newSize = newSize + img.int_size();
1001: }
1002: }
1003: return new JMLEqualsToObjectRelation(newImagePairSet, newDom,
1004: newSize);
1005: }
1006:
1007: /** Return a relation that is like this relation except that its
1008: * range is limited to just the elements of the given set.
1009: * @see #restrictDomainTo
1010: */
1011: /*@ public normal_behavior
1012: @ requires rng != null;
1013: @ ensures (\forall JMLEqualsObjectPair pair; ;
1014: @ \result.theRelation.has(pair)
1015: @ == rng.has(pair.value)
1016: @ && elementImage(pair.key).has(pair.value)
1017: @ );
1018: @*/
1019: public/*@ non_null @*/
1020: JMLEqualsToObjectRelation restrictRangeTo(
1021: /*@ non_null @*/JMLObjectSet rng) {
1022: JMLValueSet newImagePairSet = new JMLValueSet();
1023: JMLEqualsSet newDom = new JMLEqualsSet();
1024: int newSize = 0;
1025:
1026: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
1027: .imagePairs();
1028: JMLEqualsValuePair imagePair;
1029: JMLObjectSet img;
1030: while (imagePairEnum.hasMoreElements()) {
1031: imagePair = imagePairEnum.nextImagePair();
1032: img = ((JMLObjectSet) imagePair.value).intersection(rng);
1033: if (!img.isEmpty()) {
1034: newImagePairSet = newImagePairSet
1035: .insert(new JMLEqualsValuePair(imagePair.key,
1036: img));
1037: newDom = newDom.insert(imagePair.key);
1038: newSize = newSize + img.int_size();
1039: }
1040: }
1041: return new JMLEqualsToObjectRelation(newImagePairSet, newDom,
1042: newSize);
1043: }
1044:
1045: /** Return a string representation of this object.
1046: */
1047: /*@ also
1048: @ public normal_behavior
1049: @ ensures \result.equals(theRelation.toString());
1050: @*/
1051: public String toString() {
1052: return toSet().toString();
1053: }
1054:
1055: /** Return a enumerator for the set of associations that
1056: * conceptually make up this relation.
1057: * @see #elements()
1058: * @see #iterator()
1059: * @see #toSet()
1060: * @see #imagePairs()
1061: */
1062: /*@ public normal_behavior
1063: @ ensures \result != null &&
1064: @ \result.equals(new JMLEqualsToObjectRelationEnumerator(this));
1065: @*/
1066: public/*@ non_null @*/
1067: JMLEqualsToObjectRelationEnumerator associations() {
1068: return new JMLEqualsToObjectRelationEnumerator(this );
1069: }
1070:
1071: /** Return a enumerator for the set of associations that
1072: * conceptually make up this relation. This is a synonym for associations.
1073: * @see #associations()
1074: * @see #iterator()
1075: */
1076: /*@ public normal_behavior
1077: @ ensures \result != null &&
1078: @ \result.equals(associations());
1079: @*/
1080: public/*@ non_null @*/
1081: JMLEqualsToObjectRelationEnumerator elements() {
1082: return associations();
1083: }
1084:
1085: /** Returns an Iterator over the set of pairs conceptually
1086: * contained in this relation..
1087: * @see #associations()
1088: * @see #elements()
1089: */
1090: /*@ also
1091: @ public normal_behavior
1092: @ ensures \fresh(\result)
1093: @ && \result.equals(new JMLEnumerationToIterator(elements()));
1094: @*/
1095: public JMLIterator iterator() {
1096: return new JMLEnumerationToIterator(elements());
1097: }
1098:
1099: /** Return the set of all associations in this relation.
1100: * @see #associations()
1101: * @see #toBag()
1102: * @see #toSequence()
1103: */
1104: /*@ public normal_behavior
1105: @ ensures \result != null && \result.size == int_size()
1106: @ && (\forall JMLType pv; \result.has(pv);
1107: @ pv != null && pv instanceof JMLEqualsObjectPair
1108: @ && this.isDefinedAt(((JMLEqualsObjectPair)pv).key)
1109: @ && this.elementImage(((JMLEqualsObjectPair)pv).key)
1110: @ .has(((JMLEqualsObjectPair)pv).value));
1111: @
1112: @*/
1113: public/*@ non_null @*/JMLValueSet toSet() {
1114: JMLEqualsToObjectRelationEnumerator pairEnum = this
1115: .associations();
1116: JMLValueSet ret = new JMLValueSet();
1117: while (pairEnum.hasMoreElements()) {
1118: JMLEqualsObjectPair p = pairEnum.nextPair();
1119: ret = ret.insert(p);
1120: }
1121: return ret;
1122: }
1123:
1124: /** Return the bag of all associations in this relation.
1125: * @see #toSet()
1126: * @see #toSequence()
1127: */
1128: /*@ public normal_behavior
1129: @ ensures \result != null && \result.equals(toSet().toBag());
1130: @*/
1131: public/*@ non_null @*/JMLValueBag toBag() {
1132: JMLEqualsToObjectRelationEnumerator pairEnum = this
1133: .associations();
1134: JMLValueBag ret = new JMLValueBag();
1135: while (pairEnum.hasMoreElements()) {
1136: JMLEqualsObjectPair p = pairEnum.nextPair();
1137: ret = ret.insert(p);
1138: }
1139: return ret;
1140: }
1141:
1142: /** Return a sequence containing all associations in this relation.
1143: * @see #toSet()
1144: * @see #toBag()
1145: */
1146: /*@ public normal_behavior
1147: @ ensures \result != null
1148: @ && (\forall JMLEqualsObjectPair p;;
1149: @ \result.count(p) == 1 <==> this.has(p));
1150: @*/
1151: public/*@ non_null @*/JMLValueSequence toSequence() {
1152: JMLEqualsToObjectRelationEnumerator pairEnum = this
1153: .associations();
1154: JMLValueSequence ret = new JMLValueSequence();
1155: while (pairEnum.hasMoreElements()) {
1156: JMLEqualsObjectPair p = pairEnum.nextPair();
1157: ret = ret.insertFront(p);
1158: }
1159: return ret;
1160: }
1161:
1162: /** Return the set of image set pairs that make up this relation.
1163: * @see #imagePairs()
1164: * @see #toSet()
1165: */
1166: /*@ public normal_behavior
1167: @ ensures \result != null && \result.int_size() == domain().int_size()
1168: @ && (\forall Object dv; domain().has(dv);
1169: @ \result.has(
1170: @ new JMLEqualsValuePair(dv, elementImage(dv))));
1171: @*/
1172: public/*@ non_null @*/JMLValueSet imagePairSet() {
1173: return imagePairSet_;
1174: }
1175:
1176: /** Return the set of domain image set pairs that make up this relation.
1177: * @see #imagePairSet()
1178: * @see #associations()
1179: * @see #toSet()
1180: */
1181: /*@ public normal_behavior
1182: @ ensures \result != null
1183: @ && \result.abstractValue().int_size() == domain().int_size()
1184: @ && (\forall Object dv; domain().has(dv);
1185: @ \result.abstractValue().has(
1186: @ new JMLEqualsValuePair(dv, elementImage(dv))));
1187: @*/
1188: public/*@ non_null @*/
1189: JMLEqualsToObjectRelationImageEnumerator imagePairs() {
1190: return new JMLEqualsToObjectRelationImageEnumerator(this );
1191: }
1192:
1193: /** Return a enumerator for the set that is the domain of this
1194: * relation.
1195: * @see #domain()
1196: * @see #rangeElements()
1197: */
1198: /*@ public normal_behavior
1199: @ ensures \result.equals(domain().elements());
1200: @*/
1201: public/*@ non_null @*/JMLEqualsSetEnumerator domainElements() {
1202: return domain_.elements();
1203: }
1204:
1205: /** Return a enumerator for the set that is the range of this
1206: * relation. (This was formerly called "elements").
1207: * @see #range()
1208: * @see #domainElements()
1209: */
1210: /*@ public normal_behavior
1211: @ ensures \result.equals(range().elements());
1212: @*/
1213: public/*@ non_null @*/JMLObjectSetEnumerator rangeElements() {
1214: return range().elements();
1215: }
1216:
1217: /** Return the number of associations in this relation.
1218: */
1219: /*@ also
1220: @ public normal_behavior
1221: @ ensures \result == theRelation.int_size();
1222: @*/
1223: public int int_size() {
1224: return size_;
1225: }
1226:
1227: /** Return a map that is contained in this relation. If this
1228: * relation is a function, then this method can be seen as a type
1229: * conversion which does not make a change to the abstract value.
1230: * However, if this relation is not a function, then this method
1231: * chooses a function contained in this relation from among the
1232: * possibilities available.
1233: * @see #isaFunction
1234: * @see JMLEqualsToObjectMap
1235: */
1236: /*@ public normal_behavior
1237: @ ensures (\forall Object dv; dv != null;
1238: @ (this.isDefinedAt(dv) == \result.isDefinedAt(dv))
1239: @ && \result.elementImage(dv).isSubset(this.elementImage(dv))
1240: @ && \result.elementImage(dv).int_size() == 1);
1241: @*/
1242: public/*@ non_null @*/JMLEqualsToObjectMap toFunction() {
1243: JMLEqualsSet newDom = domain_;
1244: int newSize = domain_.int_size();
1245:
1246: JMLValueSet newImagePairSet = imagePairSet_;
1247:
1248: if (newSize != size_) {
1249: // Have to restrict the result to be a function
1250: JMLEqualsToObjectRelationImageEnumerator imagePairEnum = this
1251: .imagePairs();
1252: newImagePairSet = new JMLValueSet();
1253: JMLEqualsValuePair imagePair;
1254: JMLObjectSet img;
1255: while (imagePairEnum.hasMoreElements()) {
1256: imagePair = imagePairEnum.nextImagePair();
1257: img = (JMLObjectSet) imagePair.value;
1258: Enumeration imgEnum = img.elements();
1259: Object o = imgEnum.nextElement();
1260: if (o == null) {
1261: img = new JMLObjectSet(null);
1262: } else {
1263: Object rv = (Object) o;
1264: img = new JMLObjectSet(rv);
1265: }
1266: newImagePairSet = newImagePairSet
1267: .insert(new JMLEqualsValuePair(imagePair.key,
1268: img));
1269: }
1270: }
1271: return new JMLEqualsToObjectMap(newImagePairSet, newDom,
1272: newSize);
1273: }
1274: }
|