001: // @(#)$Id: JMLMap.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 _DomainType_} to non-null elements of {@link
027: * _RangeType_}. The first type, <kbd>_DomainType_</kbd>, is called
028: * the domain type of the map; the second type,
029: * <kbd>_RangeType_</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: * JML_Domain_To_Range_Relation}, and as such as can be treated as a
038: * binary relation or a set valued function also. See the
039: * documentation for {@link JML_Domain_To_Range_Relation} 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 JML_Domain_To_Range_Relation
056: * @see JML_Domain_To_Range_RelationEnumerator
057: * @see JML_Domain_To_Range_RelationImageEnumerator
058: * @see JMLValueSet
059: * @see JMLObjectSet
060: * @see JMLObjectToObjectMap
061: * @see JMLValueToObjectMap
062: * @see JMLObjectToValueMap
063: * @see JMLValueToValueMap
064: * @see JML_Domain_To_Range_Relation#toFunction()
065: */
066: //-@ immutable
067: public/*@ pure @*/
068: class JML_Domain_To_Range_Map extends JML_Domain_To_Range_Relation {
069:
070: /*@ public invariant isaFunction();
071: @ public invariant_redundantly
072: @ (\forall _DomainType_ 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 JML_Domain_To_Range_Map() {
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(_DomainType_, _RangeType_)
091: * @see #JML_Domain_To_Range_Map(JML_Domain__Range_Pair)
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 JML_Domain_To_Range_Map(/*@ non_null @*/_DomainType_ dv,
100: /*@ non_null @*/_RangeType_ 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(JML_Domain__Range_Pair)
107: * @see #JML_Domain_To_Range_Map(_DomainType_, _RangeType_)
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 JML_Domain_To_Range_Map(/*@ non_null @*/
117: JML_Domain__Range_Pair 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: @*/
127: protected JML_Domain_To_Range_Map(JMLValueSet ipset,
128: JML_Domain_Set dom, int sz) {
129: super (ipset, dom, sz);
130: }
131:
132: /** The empty JML_Domain_To_Range_Map.
133: * @see #JML_Domain_To_Range_Map()
134: */
135: public static final/*@ non_null @*/JML_Domain_To_Range_Map EMPTY = new JML_Domain_To_Range_Map();
136:
137: /** Return the singleton map containing the given association.
138: * @see #JML_Domain_To_Range_Map(_DomainType_, _RangeType_)
139: * @see #singletonMap(JML_Domain__Range_Pair)
140: */
141: /*@ public normal_behavior
142: @ requires dv != null && rv != null;
143: @ ensures \result != null
144: @ && \result.equals(new JML_Domain_To_Range_Map(dv, rv));
145: @*/
146: public static/*@ pure @*//*@ non_null @*/
147: JML_Domain_To_Range_Map singletonMap(
148: /*@ non_null @*/_DomainType_ dv,
149: /*@ non_null @*/_RangeType_ rv) {
150: return new JML_Domain_To_Range_Map(dv, rv);
151: }
152:
153: /** Return the singleton map containing the association described
154: * by the given pair.
155: * @see #JML_Domain_To_Range_Map(JML_Domain__Range_Pair)
156: * @see #singletonMap(_DomainType_, _RangeType_)
157: */
158: /*@ public normal_behavior
159: @ requires pair != null;
160: @ ensures \result != null
161: @ && \result.equals(new JML_Domain_To_Range_Map(pair));
162: @*/
163: public static/*@ pure @*//*@ non_null @*/
164: JML_Domain_To_Range_Map singletonMap(
165: /*@ non_null @*/JML_Domain__Range_Pair pair) {
166: return new JML_Domain_To_Range_Map(pair);
167: }
168:
169: /** Tells whether this relation is a function.
170: */
171: /*@ also
172: @ public normal_behavior
173: @ ensures \result;
174: @*/
175: //@ pure
176: public boolean isaFunction() {
177: return true;
178: }
179:
180: /** Return the range element corresponding to dv, if there is one.
181: *
182: * @param dv the domain element for which an association is
183: * sought (the key to the table).
184: * @exception JMLNoSuchElementException when dv is not associated
185: * to any range element by this.
186: * @see JML_Domain_To_Range_Relation#isDefinedAt
187: * @see JML_Domain_To_Range_Relation#elementImage
188: * @see JML_Domain_To_Range_Relation#image
189: */
190: /*@ public normal_behavior
191: @ requires isDefinedAt(dv);
192: @ ensures elementImage(dv).has(\result);
193: @ also
194: @ public exceptional_behavior
195: @ requires !isDefinedAt(dv);
196: @ signals (JMLNoSuchElementException);
197: @*/
198: public/*@ non_null @*/_RangeType_ apply(_DomainType_ dv)
199: throws JMLNoSuchElementException {
200: JML_Range_Set img = elementImage(dv);
201: if (img.int_size() == 1) {
202: _RangeType_ res = img.choose();
203: return res;
204: } else {
205: throw new JMLNoSuchElementException("Map not defined at "
206: + dv);
207: }
208: }
209:
210: /*@ also
211: @ public normal_behavior
212: @ ensures \result instanceof JML_Domain_To_Range_Map
213: @ && ((JML_Domain_To_Range_Map)\result)
214: @ .theRelation.equals(this.theRelation);
215: @*/
216: //@ pure
217: public Object clone() {
218: return new JML_Domain_To_Range_Map(imagePairSet_, domain_,
219: size_);
220: }
221:
222: /** Return a new map that is like this but maps the given domain
223: * element to the given range element. Any previously existing
224: * mapping for the domain element is removed first.
225: * @see JML_Domain_To_Range_Relation#insert(_DomainType_, _RangeType_)
226: */
227: /*@ public normal_behavior
228: @ requires dv != null && rv != null;
229: @ requires !isDefinedAt(dv) ==> int_size() < Integer.MAX_VALUE;
230: @ ensures \result.equals(this.removeDomainElement(dv).add(dv, rv));
231: @*/
232: public/*@ non_null @*/
233: JML_Domain_To_Range_Map extend(/*@ non_null @*/_DomainType_ dv,
234: /*@ non_null @*/_RangeType_ rv) {
235: JML_Domain_To_Range_Map newMap = this .removeDomainElement(dv);
236: newMap = newMap.disjointUnion(new JML_Domain_To_Range_Map(dv,
237: rv));
238: return newMap;
239: }
240:
241: /** Return a new map that is like this but has no association for the
242: * given domain element.
243: * @see JML_Domain_To_Range_Relation#removeFromDomain
244: */
245: /*@ public normal_behavior
246: @ ensures \result.equals(removeFromDomain(dv).toFunction());
247: @ ensures_redundantly !isDefinedAt(dv) ==> \result.equals(this);
248: @*/
249: public/*@ non_null @*/
250: JML_Domain_To_Range_Map removeDomainElement(_DomainType_ dv) {
251: return super .removeFromDomain(dv).toFunction();
252: }
253:
254: /** Return a new map that is the composition of this and the given
255: * map. The composition is done in the usual order; that is, if
256: * the given map maps x to y and this maps y to z, then the
257: * result maps x to z.
258: * @see #compose(JMLObjectTo_Domain_Map)
259: */
260: /*@ public normal_behavior
261: @ requires othMap != null;
262: @ ensures (\forall JMLValue_Range_Pair pair; ;
263: @ \result.theRelation.has(pair)
264: @ == (\exists _DomainType_ val;
265: @ othMap.elementImage(pair.key).has(val);
266: @ this.elementImage(val).has(pair.value)
267: @ )
268: @ );
269: @*/
270: public/*@ non_null @*/
271: JMLValueTo_Range_Map compose(
272: /*@ non_null @*/JMLValueTo_Domain_Map othMap) {
273: return super .compose(othMap).toFunction();
274: }
275:
276: /** Return a new map that is the composition of this and the given
277: * map. The composition is done in the usual order; that is, if
278: * the given map maps x to y and this maps y to z, then the
279: * result maps x to z.
280: * @see #compose(JMLValueTo_Domain_Map)
281: */
282: /*@ public normal_behavior
283: @ requires othMap != null;
284: @ ensures (\forall JMLObject_Range_Pair pair; ;
285: @ \result.theRelation.has(pair)
286: @ == (\exists _DomainType_ val;
287: @ othMap.elementImage(pair.key).has(val);
288: @ this.elementImage(val).has(pair.value)
289: @ )
290: @ );
291: @*/
292: public/*@ non_null @*/
293: JMLObjectTo_Range_Map compose(
294: /*@ non_null @*/JMLObjectTo_Domain_Map othMap) {
295: return super .compose(othMap).toFunction();
296: }
297:
298: /** Return a new map that only maps elements in the given domain
299: * to the corresponding range elements in this map.
300: * @see #rangeRestrictedTo
301: * @see JML_Domain_To_Range_Relation#restrictDomainTo
302: */
303: /*@ public normal_behavior
304: @ requires dom != null;
305: @ ensures (\forall JML_Domain__Range_Pair pair; ;
306: @ \result.theRelation.has(pair)
307: @ ==
308: @ dom.has(pair.key)
309: @ && elementImage(pair.key).has(pair.value)
310: @ );
311: @*/
312: public/*@ non_null @*/
313: JML_Domain_To_Range_Map restrictedTo(
314: /*@ non_null @*/JML_Domain_Set dom) {
315: return super .restrictDomainTo(dom).toFunction();
316: }
317:
318: /** Return a new map that is like this map but only contains
319: * associations that map to range elements in the given set.
320: * @see #restrictedTo
321: * @see JML_Domain_To_Range_Relation#restrictRangeTo
322: */
323: /*@ public normal_behavior
324: @ requires rng != null;
325: @ ensures (\forall JML_Domain__Range_Pair pair; ;
326: @ \result.theRelation.has(pair)
327: @ ==
328: @ rng.has(pair.value)
329: @ && elementImage(pair.key).has(pair.value)
330: @ );
331: @*/
332: public/*@ non_null @*/
333: JML_Domain_To_Range_Map rangeRestrictedTo(
334: /*@ non_null @*/JML_Range_Set rng) {
335: return super .restrictRangeTo(rng).toFunction();
336: }
337:
338: /** Return a new map that is like the union of the given map and
339: * this map, except that if both define a mapping for a given domain
340: * element, then only the mapping in the given map is retained.
341: * @see #clashReplaceUnion
342: * @see #disjointUnion
343: * @see JML_Domain_To_Range_Relation#union
344: */
345: /*@ public normal_behavior
346: @ requires othMap != null;
347: @ requires int_size()
348: @ <= Integer.MAX_VALUE - othMap.difference(this).int_size();
349: @ ensures (\forall JML_Domain__Range_Pair pair; ;
350: @ \result.theRelation.has(pair)
351: @ ==
352: @ othMap.elementImage(pair.key).has(pair.value)
353: @ || (!othMap.isDefinedAt(pair.key)
354: @ && this.elementImage(pair.key).has(pair.value))
355: @ );
356: @*/
357: public/*@ non_null @*/
358: JML_Domain_To_Range_Map extendUnion(
359: /*@ non_null @*/JML_Domain_To_Range_Map othMap)
360: throws IllegalStateException {
361: JML_Domain_To_Range_Map newMap = this .restrictedTo(this .domain_
362: .difference(othMap.domain_));
363: if (newMap.size_ <= Integer.MAX_VALUE - othMap.size_) {
364: return new JML_Domain_To_Range_Map(newMap.imagePairSet_
365: .union(othMap.imagePairSet_), newMap.domain_
366: .union(othMap.domain_), newMap.size_ + othMap.size_);
367: } else {
368: throw new IllegalStateException(TOO_BIG_TO_UNION);
369: }
370: }
371:
372: /** Return a new map that is like the union of the given map and
373: * this map, except that if both define a mapping for a given
374: * domain element, then each of these clashes is replaced by a
375: * mapping from the domain element in question to the given range
376: * element.
377: * @param othMap the other map.
378: * @param errval the range element to use when clashes occur.
379: * @see #extendUnion
380: * @see #disjointUnion
381: * @see JML_Domain_To_Range_Relation#union
382: */
383: /*@ public normal_behavior
384: @ requires othMap != null && errval != null;
385: @ requires int_size()
386: @ <= Integer.MAX_VALUE - othMap.difference(this).int_size();
387: @ ensures (\forall JML_Domain__Range_Pair pair; ;
388: @ \result.theRelation.has(pair)
389: @ ==
390: @ (!othMap.isDefinedAt(pair.key)
391: @ && this.elementImage(pair.key).has(pair.value))
392: @ || (!this.isDefinedAt(pair.key)
393: @ && othMap.elementImage(pair.key)
394: @ .has(pair.value))
395: @ || (this.isDefinedAt(pair.key)
396: @ && othMap.isDefinedAt(pair.key)
397: @ && pair.value _rangeEquals_ (errval))
398: @ );
399: @ implies_that
400: @ requires othMap != null && errval != null;
401: @*/
402: public/*@ non_null @*/
403: JML_Domain_To_Range_Map clashReplaceUnion(
404: JML_Domain_To_Range_Map othMap, _RangeType_ errval)
405: throws IllegalStateException {
406: JML_Domain_Set overlap = this .domain_
407: .intersection(othMap.domain_);
408: Enumeration overlapEnum = overlap.elements();
409: othMap = othMap
410: .restrictedTo(othMap.domain_.difference(overlap));
411: JML_Domain_To_Range_Map newMap = this .restrictedTo(this .domain_
412: .difference(overlap));
413: JML_Domain_To_Range_Relation newRel;
414: if (newMap.size_ <= Integer.MAX_VALUE - othMap.size_) {
415: newRel = new JML_Domain_To_Range_Relation(
416: newMap.imagePairSet_.union(othMap.imagePairSet_),
417: newMap.domain_.union(othMap.domain_), newMap.size_
418: + othMap.size_);
419: } else {
420: throw new IllegalStateException(TOO_BIG_TO_UNION);
421: }
422: _DomainType_ dv;
423: while (overlapEnum.hasMoreElements()) {
424: Object oo = overlapEnum.nextElement();
425: dv = (_DomainType_) oo;
426: newRel = newRel.add(dv, errval);
427: }
428: return newRel.toFunction();
429: }
430:
431: /** Return a map that is the disjoint union of this and othMap.
432: * @param othMap the other mapping
433: * @exception JMLMapException the ranges of this and othMap have elements
434: * in common (i.e., when they interesect).
435: * @see #extendUnion
436: * @see #clashReplaceUnion
437: * @see JML_Domain_To_Range_Relation#union
438: */
439: /*@ public normal_behavior
440: @ requires othMap != null
441: @ && this.domain().intersection(othMap.domain()).isEmpty();
442: @ requires int_size() <= Integer.MAX_VALUE - othMap.int_size();
443: @ ensures \result.equals(this.union(othMap));
444: @ also
445: @ public exceptional_behavior
446: @ requires othMap != null
447: @ && !this.domain().intersection(othMap.domain()).isEmpty();
448: @ signals (JMLMapException);
449: @*/
450: public/*@ non_null @*/
451: JML_Domain_To_Range_Map disjointUnion(
452: /*@ non_null @*/JML_Domain_To_Range_Map othMap)
453: throws JMLMapException, IllegalStateException {
454: JML_Domain_Set overlappingDom = domain_
455: .intersection(othMap.domain_);
456: if (overlappingDom.isEmpty()) {
457: if (this .size_ <= Integer.MAX_VALUE - othMap.size_) {
458: return new JML_Domain_To_Range_Map(this .imagePairSet_
459: .union(othMap.imagePairSet_), this .domain_
460: .union(othMap.domain_), this .size_
461: + othMap.size_);
462: } else {
463: throw new IllegalStateException(TOO_BIG_TO_UNION);
464: }
465: } else {
466: throw new JMLMapException("Overlapping domains in "
467: + " disjointUnion operation", overlappingDom);
468: }
469: }
470:
471: }
|