001: // @(#)$Id: JMLValueToEqualsMap.java 1.2 Wed, 25 May 2005 14:55:29 +0200 engelc $
002:
003: // Copyright (C) 1998, 1999, 2002 Iowa State University
004:
005: // This file is part of JML
006:
007: // JML is free software; you can redistribute it and/or modify
008: // it under the terms of the GNU General Public License as published by
009: // the Free Software Foundation; either version 2, or (at your option)
010: // any later version.
011:
012: // JML is distributed in the hope that it will be useful,
013: // but WITHOUT ANY WARRANTY; without even the implied warranty of
014: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
015: // GNU General Public License for more details.
016:
017: // You should have received a copy of the GNU General Public License
018: // along with JML; see the file COPYING. If not, write to
019: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
020:
021: package org.jmlspecs.models;
022:
023: import java.util.Enumeration;
024:
025: /** Maps (i.e., binary relations that are functional) from non-null
026: * elements of {@link JMLType} to non-null elements of {@link
027: * Object}. The first type, <kbd>JMLType</kbd>, is called
028: * the domain type of the map; the second type,
029: * <kbd>Object</kbd>, is called the range type of the map. A
030: * map can be seen as a set of pairs, of form <em>(dv, rv)</em>,
031: * consisting of an element of the domain type, <em>dv</em>, and an
032: * element of the range type, <em>rv</em>. Alternatively, it can be
033: * seen as a function that maps each element of the domain to some of
034: * elements of the range type.
035: *
036: * <p> This type is a subtype of {@link
037: * JMLValueToEqualsRelation}, and as such as can be treated as a
038: * binary relation or a set valued function also. See the
039: * documentation for {@link JMLValueToEqualsRelation} and for the
040: * methods inherited from this supertype for more information.
041: *
042: * <p> This type considers elements <kbd>val</kbd> and <kbd>dv</kbd>
043: * of the domain type, to be distinct just when
044: * <kbd>_val_not_equal_to_dv_</kbd>. It considers elements of
045: * <kbd>r</kbd> and <kbd>rv</kbd> of the range type to be distinct
046: * just when <kbd>_r_not_equal_to_rv_</kbd>. Cloning takes place for
047: * the domain or range elements if the corresponding domain or range
048: * type is {@link JMLType}.
049: *
050: * @version $Revision: 1.2 $
051: * @author Gary T. Leavens
052: * @author Clyde Ruby
053: * @see JMLCollection
054: * @see JMLType
055: * @see JMLValueToEqualsRelation
056: * @see JMLValueToEqualsRelationEnumerator
057: * @see JMLValueToEqualsRelationImageEnumerator
058: * @see JMLValueSet
059: * @see JMLObjectSet
060: * @see JMLObjectToObjectMap
061: * @see JMLValueToObjectMap
062: * @see JMLObjectToValueMap
063: * @see JMLValueToValueMap
064: * @see JMLValueToEqualsRelation#toFunction()
065: */
066: //-@ immutable
067: public/*@ pure @*/
068: class JMLValueToEqualsMap extends JMLValueToEqualsRelation {
069:
070: /*@ public invariant isaFunction();
071: @ public invariant_redundantly
072: @ (\forall JMLType dv; isDefinedAt(dv);
073: @ elementImage(dv).int_size() == 1);
074: @*/
075:
076: /** Initialize this map to be the empty mapping.
077: * @see #EMPTY
078: */
079: /*@ public normal_behavior
080: @ assignable theRelation, owner, elementType, containsNull;
081: @ ensures theRelation.equals(new JMLValueSet());
082: @ ensures_redundantly theRelation.isEmpty();
083: @*/
084: public JMLValueToEqualsMap() {
085: super ();
086: }
087:
088: /** Initialize this map to be a mapping that maps the given domain
089: * element to the given range element.
090: * @see #singletonMap(JMLType, Object)
091: * @see #JMLValueToEqualsMap(JMLValueEqualsPair)
092: */
093: /*@ public normal_behavior
094: @ requires dv != null && rv != null;
095: @ assignable theRelation, owner, elementType, containsNull;
096: @ ensures (theRelation.int_size() == 1) && elementImage(dv).has(rv);
097: @ ensures_redundantly isDefinedAt(dv);
098: @*/
099: public JMLValueToEqualsMap(/*@ non_null @*/JMLType dv,
100: /*@ non_null @*/Object rv) {
101: super (dv, rv);
102: }
103:
104: /** Initialize this map to be a mapping that maps the key in the
105: * given pair to the value in that pair.
106: * @see #singletonMap(JMLValueEqualsPair)
107: * @see #JMLValueToEqualsMap(JMLType, Object)
108: */
109: /*@ public normal_behavior
110: @ requires pair != null;
111: @ assignable theRelation, owner, elementType, containsNull;
112: @ ensures (theRelation.int_size() == 1)
113: @ && elementImage(pair.key).has(pair.value);
114: @ ensures_redundantly isDefinedAt(pair.key);
115: @*/
116: public JMLValueToEqualsMap(/*@ non_null @*/
117: JMLValueEqualsPair pair) {
118: super (pair.key, pair.value);
119: }
120:
121: /** Initialize this map based on the representation values given.
122: */
123: //@ requires ipset != null && dom != null && 0 <= sz;
124: //@ assignable theRelation, owner, elementType, containsNull;
125: //@ ensures imagePairSet_ == ipset && domain_ == dom && size_ == sz;
126: protected JMLValueToEqualsMap(JMLValueSet ipset, JMLValueSet dom,
127: int sz) {
128: super (ipset, dom, sz);
129: }
130:
131: /** The empty JMLValueToEqualsMap.
132: * @see #JMLValueToEqualsMap()
133: */
134: public static final/*@ non_null @*/JMLValueToEqualsMap EMPTY = new JMLValueToEqualsMap();
135:
136: /** Return the singleton map containing the given association.
137: * @see #JMLValueToEqualsMap(JMLType, Object)
138: * @see #singletonMap(JMLValueEqualsPair)
139: */
140: /*@ public normal_behavior
141: @ requires dv != null && rv != null;
142: @ ensures \result != null
143: @ && \result.equals(new JMLValueToEqualsMap(dv, rv));
144: @*/
145: public static/*@ pure @*//*@ non_null @*/
146: JMLValueToEqualsMap singletonMap(/*@ non_null @*/JMLType dv,
147: /*@ non_null @*/Object rv) {
148: return new JMLValueToEqualsMap(dv, rv);
149: }
150:
151: /** Return the singleton map containing the association described
152: * by the given pair.
153: * @see #JMLValueToEqualsMap(JMLValueEqualsPair)
154: * @see #singletonMap(JMLType, Object)
155: */
156: /*@ public normal_behavior
157: @ requires pair != null;
158: @ ensures \result != null
159: @ && \result.equals(new JMLValueToEqualsMap(pair));
160: @*/
161: public static/*@ pure @*//*@ non_null @*/
162: JMLValueToEqualsMap singletonMap(
163: /*@ non_null @*/JMLValueEqualsPair pair) {
164: return new JMLValueToEqualsMap(pair);
165: }
166:
167: /** Tells whether this relation is a function.
168: */
169: /*@ also
170: @ public normal_behavior
171: @ ensures \result;
172: @*/
173: //@ pure
174: public boolean isaFunction() {
175: return true;
176: }
177:
178: /** Return the range element corresponding to dv, if there is one.
179: *
180: * @param dv the domain element for which an association is
181: * sought (the key to the table).
182: * @exception JMLNoSuchElementException when dv is not associated
183: * to any range element by this.
184: * @see JMLValueToEqualsRelation#isDefinedAt
185: * @see JMLValueToEqualsRelation#elementImage
186: * @see JMLValueToEqualsRelation#image
187: */
188: /*@ public normal_behavior
189: @ requires isDefinedAt(dv);
190: @ ensures elementImage(dv).has(\result);
191: @ also
192: @ public exceptional_behavior
193: @ requires !isDefinedAt(dv);
194: @ signals (JMLNoSuchElementException);
195: @*/
196: public/*@ non_null @*/Object apply(JMLType dv)
197: throws JMLNoSuchElementException {
198: JMLEqualsSet img = elementImage(dv);
199: if (img.int_size() == 1) {
200: Object res = img.choose();
201: return res;
202: } else {
203: throw new JMLNoSuchElementException("Map not defined at "
204: + dv);
205: }
206: }
207:
208: /*@ also
209: @ public normal_behavior
210: @ ensures \result instanceof JMLValueToEqualsMap
211: @ && ((JMLValueToEqualsMap)\result)
212: @ .theRelation.equals(this.theRelation);
213: @*/
214: //@ pure
215: public Object clone() {
216: return new JMLValueToEqualsMap(imagePairSet_, domain_, size_);
217: }
218:
219: /** Return a new map that is like this but maps the given domain
220: * element to the given range element. Any previously existing
221: * mapping for the domain element is removed first.
222: * @see JMLValueToEqualsRelation#insert(JMLType, Object)
223: */
224: /*@ public normal_behavior
225: @ requires dv != null && rv != null;
226: @ requires !isDefinedAt(dv) ==> int_size() < Integer.MAX_VALUE;
227: @ ensures \result.equals(this.removeDomainElement(dv).add(dv, rv));
228: @*/
229: public/*@ non_null @*/
230: JMLValueToEqualsMap extend(/*@ non_null @*/JMLType dv,
231: /*@ non_null @*/Object rv) {
232: JMLValueToEqualsMap newMap = this .removeDomainElement(dv);
233: newMap = newMap.disjointUnion(new JMLValueToEqualsMap(dv, rv));
234: return newMap;
235: }
236:
237: /** Return a new map that is like this but has no association for the
238: * given domain element.
239: * @see JMLValueToEqualsRelation#removeFromDomain
240: */
241: /*@ public normal_behavior
242: @ ensures \result.equals(removeFromDomain(dv).toFunction());
243: @ ensures_redundantly !isDefinedAt(dv) ==> \result.equals(this);
244: @*/
245: public/*@ non_null @*/
246: JMLValueToEqualsMap removeDomainElement(JMLType dv) {
247: return super .removeFromDomain(dv).toFunction();
248: }
249:
250: /** Return a new map that is the composition of this and the given
251: * map. The composition is done in the usual order; that is, if
252: * the given map maps x to y and this maps y to z, then the
253: * result maps x to z.
254: * @see #compose(JMLObjectToValueMap)
255: */
256: /*@ public normal_behavior
257: @ requires othMap != null;
258: @ ensures (\forall JMLValueEqualsPair pair; ;
259: @ \result.theRelation.has(pair)
260: @ == (\exists JMLType val;
261: @ othMap.elementImage(pair.key).has(val);
262: @ this.elementImage(val).has(pair.value)
263: @ )
264: @ );
265: @*/
266: public/*@ non_null @*/
267: JMLValueToEqualsMap compose(
268: /*@ non_null @*/JMLValueToValueMap othMap) {
269: return super .compose(othMap).toFunction();
270: }
271:
272: /** Return a new map that is the composition of this and the given
273: * map. The composition is done in the usual order; that is, if
274: * the given map maps x to y and this maps y to z, then the
275: * result maps x to z.
276: * @see #compose(JMLValueToValueMap)
277: */
278: /*@ public normal_behavior
279: @ requires othMap != null;
280: @ ensures (\forall JMLObjectEqualsPair pair; ;
281: @ \result.theRelation.has(pair)
282: @ == (\exists JMLType val;
283: @ othMap.elementImage(pair.key).has(val);
284: @ this.elementImage(val).has(pair.value)
285: @ )
286: @ );
287: @*/
288: public/*@ non_null @*/
289: JMLObjectToEqualsMap compose(
290: /*@ non_null @*/JMLObjectToValueMap othMap) {
291: return super .compose(othMap).toFunction();
292: }
293:
294: /** Return a new map that only maps elements in the given domain
295: * to the corresponding range elements in this map.
296: * @see #rangeRestrictedTo
297: * @see JMLValueToEqualsRelation#restrictDomainTo
298: */
299: /*@ public normal_behavior
300: @ requires dom != null;
301: @ ensures (\forall JMLValueEqualsPair pair; ;
302: @ \result.theRelation.has(pair)
303: @ ==
304: @ dom.has(pair.key)
305: @ && elementImage(pair.key).has(pair.value)
306: @ );
307: @*/
308: public/*@ non_null @*/
309: JMLValueToEqualsMap restrictedTo(/*@ non_null @*/JMLValueSet dom) {
310: return super .restrictDomainTo(dom).toFunction();
311: }
312:
313: /** Return a new map that is like this map but only contains
314: * associations that map to range elements in the given set.
315: * @see #restrictedTo
316: * @see JMLValueToEqualsRelation#restrictRangeTo
317: */
318: /*@ public normal_behavior
319: @ requires rng != null;
320: @ ensures (\forall JMLValueEqualsPair pair; ;
321: @ \result.theRelation.has(pair)
322: @ ==
323: @ rng.has(pair.value)
324: @ && elementImage(pair.key).has(pair.value)
325: @ );
326: @*/
327: public/*@ non_null @*/
328: JMLValueToEqualsMap rangeRestrictedTo(
329: /*@ non_null @*/JMLEqualsSet rng) {
330: return super .restrictRangeTo(rng).toFunction();
331: }
332:
333: /** Return a new map that is like the union of the given map and
334: * this map, except that if both define a mapping for a given domain
335: * element, then only the mapping in the given map is retained.
336: * @see #clashReplaceUnion
337: * @see #disjointUnion
338: * @see JMLValueToEqualsRelation#union
339: */
340: /*@ public normal_behavior
341: @ requires othMap != null;
342: @ requires int_size()
343: @ <= Integer.MAX_VALUE - othMap.difference(this).int_size();
344: @ ensures (\forall JMLValueEqualsPair pair; ;
345: @ \result.theRelation.has(pair)
346: @ ==
347: @ othMap.elementImage(pair.key).has(pair.value)
348: @ || (!othMap.isDefinedAt(pair.key)
349: @ && this.elementImage(pair.key).has(pair.value))
350: @ );
351: @*/
352: public/*@ non_null @*/
353: JMLValueToEqualsMap extendUnion(
354: /*@ non_null @*/JMLValueToEqualsMap othMap)
355: throws IllegalStateException {
356: JMLValueToEqualsMap newMap = this .restrictedTo(this .domain_
357: .difference(othMap.domain_));
358: if (newMap.size_ <= Integer.MAX_VALUE - othMap.size_) {
359: return new JMLValueToEqualsMap(newMap.imagePairSet_
360: .union(othMap.imagePairSet_), newMap.domain_
361: .union(othMap.domain_), newMap.size_ + othMap.size_);
362: } else {
363: throw new IllegalStateException(TOO_BIG_TO_UNION);
364: }
365: }
366:
367: /** Return a new map that is like the union of the given map and
368: * this map, except that if both define a mapping for a given
369: * domain element, then each of these clashes is replaced by a
370: * mapping from the domain element in question to the given range
371: * element.
372: * @param othMap the other map.
373: * @param errval the range element to use when clashes occur.
374: * @see #extendUnion
375: * @see #disjointUnion
376: * @see JMLValueToEqualsRelation#union
377: */
378: /*@ public normal_behavior
379: @ requires othMap != null && errval != null;
380: @ requires int_size()
381: @ <= Integer.MAX_VALUE - othMap.difference(this).int_size();
382: @ ensures (\forall JMLValueEqualsPair pair; ;
383: @ \result.theRelation.has(pair)
384: @ ==
385: @ (!othMap.isDefinedAt(pair.key)
386: @ && this.elementImage(pair.key).has(pair.value))
387: @ || (!this.isDefinedAt(pair.key)
388: @ && othMap.elementImage(pair.key)
389: @ .has(pair.value))
390: @ || (this.isDefinedAt(pair.key)
391: @ && othMap.isDefinedAt(pair.key)
392: @ && pair.value .equals(errval))
393: @ );
394: @ implies_that
395: @ requires othMap != null && errval != null;
396: @*/
397: public/*@ non_null @*/
398: JMLValueToEqualsMap clashReplaceUnion(JMLValueToEqualsMap othMap,
399: Object errval) throws IllegalStateException {
400: JMLValueSet overlap = this .domain_.intersection(othMap.domain_);
401: Enumeration overlapEnum = overlap.elements();
402: othMap = othMap
403: .restrictedTo(othMap.domain_.difference(overlap));
404: JMLValueToEqualsMap newMap = this .restrictedTo(this .domain_
405: .difference(overlap));
406: JMLValueToEqualsRelation newRel;
407: if (newMap.size_ <= Integer.MAX_VALUE - othMap.size_) {
408: newRel = new JMLValueToEqualsRelation(newMap.imagePairSet_
409: .union(othMap.imagePairSet_), newMap.domain_
410: .union(othMap.domain_), newMap.size_ + othMap.size_);
411: } else {
412: throw new IllegalStateException(TOO_BIG_TO_UNION);
413: }
414: JMLType dv;
415: while (overlapEnum.hasMoreElements()) {
416: Object oo = overlapEnum.nextElement();
417: dv = (JMLType) oo;
418: newRel = newRel.add(dv, errval);
419: }
420: return newRel.toFunction();
421: }
422:
423: /** Return a map that is the disjoint union of this and othMap.
424: * @param othMap the other mapping
425: * @exception JMLMapException the ranges of this and othMap have elements
426: * in common (i.e., when they interesect).
427: * @see #extendUnion
428: * @see #clashReplaceUnion
429: * @see JMLValueToEqualsRelation#union
430: */
431: /*@ public normal_behavior
432: @ requires othMap != null
433: @ && this.domain().intersection(othMap.domain()).isEmpty();
434: @ requires int_size() <= Integer.MAX_VALUE - othMap.int_size();
435: @ ensures \result.equals(this.union(othMap));
436: @ also
437: @ public exceptional_behavior
438: @ requires othMap != null
439: @ && !this.domain().intersection(othMap.domain()).isEmpty();
440: @ signals (JMLMapException);
441: @*/
442: public/*@ non_null @*/
443: JMLValueToEqualsMap disjointUnion(
444: /*@ non_null @*/JMLValueToEqualsMap othMap)
445: throws JMLMapException, IllegalStateException {
446: JMLValueSet overlappingDom = domain_
447: .intersection(othMap.domain_);
448: if (overlappingDom.isEmpty()) {
449: if (this .size_ <= Integer.MAX_VALUE - othMap.size_) {
450: return new JMLValueToEqualsMap(this .imagePairSet_
451: .union(othMap.imagePairSet_), this .domain_
452: .union(othMap.domain_), this .size_
453: + othMap.size_);
454: } else {
455: throw new IllegalStateException(TOO_BIG_TO_UNION);
456: }
457: } else {
458: throw new JMLMapException("Overlapping domains in "
459: + " disjointUnion operation", overlappingDom);
460: }
461: }
462:
463: }
|