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