001: // @(#)$Id: JMLValueSet.java 1.2 Mon, 09 May 2005 15:27:50 +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: /** Sets of values. This type uses ".equals" to
026: * compare elements, and clones elements that are passed into and
027: * returned from the set's methods.
028: *
029: * <p>
030: * For the purposes of informal specification in the methods below, we
031: * assume there is a model field
032: * <pre>public model mathematical_set theSet;</pre>
033: * that you can think of as a mathematical set of values.
034: *
035: * @version $Revision: 1.2 $
036: * @author Gary T. Leavens, with help from Albert Baker, Clyde Ruby,
037: * and others.
038: * @see JMLCollection
039: * @see JMLType
040: * @see JMLEqualsSet
041: * @see JMLObjectSet
042: * @see JMLValueSetEnumerator
043: * @see JMLValueSetSpecs
044: * @see JMLObjectBag
045: * @see JMLEqualsBag
046: * @see JMLValueBag
047: */
048: //-@ immutable
049: public/*@ pure @*/class JMLValueSet extends JMLValueSetSpecs implements
050: JMLCollection {
051:
052: //*********************** equational theory ***********************
053:
054: /*@ public invariant (\forall JMLValueSet s2; s2 != null;
055: @ (\forall JMLType e1, e2; ;
056: @ equational_theory(this, s2, e1, e2) ));
057: @*/
058:
059: /** An equational specification of the properties of sets.
060: */
061: /*@ public normal_behavior
062: @ {|
063: @ // The following are defined by using has and induction.
064: @
065: @ ensures \result <==> !(new JMLValueSet()).has(e1);
066: @ also
067: @ ensures \result <==>
068: @ s.insert(null).has(e2) == (e2 == null || s.has(e2));
069: @ also
070: @ ensures \result <==>
071: @ (e1 != null
072: @ ==> s.insert(e1).has(e2)
073: @ == (e1.equals(e2) || s.has(e2)));
074: @ also
075: @ ensures \result <==>
076: @ (new JMLValueSet()).int_size() == 0;
077: @ also
078: @ ensures \result <==>
079: @ s.insert(e1).int_size()
080: @ == (s.has(e1) ? s.int_size() : s.int_size() + 1);
081: @ also
082: @ ensures \result <==>
083: @ s.isSubset(s2)
084: @ == (\forall JMLType o; ; s.has(o) ==> s2.has(o));
085: @ also
086: @ ensures \result <==>
087: @ s.equals(s2) == (s.isSubset(s2) && s2.isSubset(s));
088: @ also
089: @ ensures \result <==>
090: @ (new JMLValueSet()).remove(e1).equals(new JMLValueSet());
091: @ also
092: @ ensures \result <==>
093: @ s.insert(null).remove(e2)
094: @ .equals
095: @ (e2 == null ? s : s.remove(e2).insert(null));
096: @ also
097: @ ensures \result <==>
098: @ e1 != null
099: @ ==> s.insert(e1).remove(e2)
100: @ .equals
101: @ (e1.equals(e2)
102: @ ? s : s.remove(e2).insert(e1));
103: @ also
104: @ ensures \result <==>
105: @ (s.union(s2)).has(e1) == (s.has(e1) || s2.has(e1));
106: @ also
107: @ ensures \result <==>
108: @ (s.intersection(s2)).has(e1) == (s.has(e1) && s2.has(e1));
109: @ also
110: @ ensures \result <==>
111: @ (s.difference(s2)).has(e1) == (s.has(e1) && !s2.has(e1));
112: @
113: @
114: @ // The following are all defined as abbreviations.
115: @
116: @ also
117: @ ensures \result <==>
118: @ s.isEmpty() == (s.int_size() == 0);
119: @ also
120: @ ensures \result <==>
121: @ (new JMLValueSet(e1)).equals(new JMLValueSet().insert(e1));
122: @ also
123: @ ensures \result <==>
124: @ s.isProperSubset(s2)
125: @ == ( s.isSubset(s2) && !s.equals(s2));
126: @ also
127: @ ensures \result <==>
128: @ s.isSuperset(s2) == s2.isSubset(s);
129: @ also
130: @ ensures \result <==>
131: @ s.isProperSuperset(s2) == s2.isProperSubset(s);
132: @ |}
133: @
134: static public pure model boolean equational_theory(JMLValueSet s,
135: JMLValueSet s2,
136: JMLType e1,
137: JMLType e2);
138: @*/
139:
140: //@ public invariant elementType <: \type(JMLType);
141: /*@ public invariant
142: @ (\forall JMLType o; o != null && has(o);
143: @ \typeof(o) <: elementType);
144: @*/
145:
146: //@ public invariant containsNull <==> has(null);
147: //@ public invariant_redundantly isEmpty() ==> !containsNull;
148: /** The list representing the elements of this set.
149: */
150: protected final JMLListValueNode the_list;
151: //@ in objectState;
152:
153: /** The number of elements in this set.
154: */
155: /*@ spec_public @*/protected final int size;
156:
157: //@ in objectState;
158:
159: //@ protected invariant the_list == null ==> size == 0;
160: //@ protected invariant the_list != null ==> size == the_list.int_size();
161: //@ protected invariant (the_list == null) == (size == 0);
162: //@ protected invariant size >= 0;
163: /*@ protected invariant the_list != null && the_list.next != null ==>
164: @ !the_list.next.has(the_list.val);
165: @*/
166:
167: //@ protected invariant size == 0 ==> !containsNull;
168: //@ public invariant owner == null;
169: //************************* Constructors ********************************
170: /** Initialize this to be an empty set.
171: * @see #EMPTY
172: */
173: /*@ public normal_behavior
174: @ assignable objectState, elementType, containsNull, owner;
175: @ ensures this.isEmpty();
176: @*/
177: public JMLValueSet() {
178: the_list = null;
179: size = 0;
180: }
181:
182: /*@ public normal_behavior
183: @ assignable objectState, elementType, containsNull, owner;
184: @ ensures this.has(e) && this.int_size() == 1;
185: @*/
186: public JMLValueSet(JMLType e) {
187: the_list = JMLListValueNode.cons(e, null); // cons() clones if needed
188: size = 1;
189: }
190:
191: /*@ requires (ls == null) == (sz == 0);
192: @ requires sz >= 0;
193: @ assignable objectState, elementType, containsNull, owner;
194: @ ensures ls != null ==> elementType == ls.elementType;
195: @ ensures ls != null ==> containsNull == ls.containsNull;
196: @ ensures ls == null ==> elementType <: \type(JMLType);
197: @ ensures ls == null ==> !containsNull;
198: @*/
199: protected JMLValueSet(JMLListValueNode ls, int sz) {
200: the_list = ls;
201: size = sz;
202: }
203:
204: /*@ assignable objectState, elementType, containsNull, owner;
205: @ ensures ls != null ==> elementType == ls.elementType;
206: @ ensures ls != null ==> containsNull == ls.containsNull;
207: @ ensures ls == null ==> elementType <: \type(JMLType);
208: @ ensures ls == null ==> !containsNull;
209: @*/
210: protected JMLValueSet(JMLListValueNode ls) {
211: this (ls, (ls == null) ? 0 : ls.int_size());
212: }
213:
214: //**************************** Static methods ****************************
215:
216: /** The empty JMLValueSet.
217: * @see #JMLValueSet()
218: */
219: public static final/*@ non_null @*/JMLValueSet EMPTY = new JMLValueSet();
220:
221: /** Return the singleton set containing the given element.
222: * @see #JMLValueSet(JMLType)
223: */
224: /*@ public normal_behavior
225: @ ensures \result != null && \result.equals(new JMLValueSet(e));
226: @*/
227: public static/*@ pure @*//*@ non_null @*/
228: JMLValueSet singleton(JMLType e) {
229: return new JMLValueSet(e);
230: }
231:
232: /** Return the set containing all the elements in the given array.
233: */
234: /*@ public normal_behavior
235: @ requires a != null;
236: @ ensures \result != null && \result.int_size() == a.length
237: @ && (\forall int i; 0 <= i && i < a.length; \result.has(a[i]));
238: @*/
239: public static/*@ pure @*//*@ non_null @*/
240: JMLValueSet convertFrom(/*@ non_null @*/JMLType[] a) {
241: /*@ non_null @*/JMLValueSet ret = EMPTY;
242: for (int i = 0; i < a.length; i++) {
243: ret = ret.insert(a[i]);
244: }
245: return ret;
246: }
247:
248: /** Return the set containing all the value in the
249: * given collection.
250: * @throws ClassCastException if some element in c is not an instance of
251: * JMLType.
252: * @see #containsAll(java.util.Collection)
253: */
254: /*@ public normal_behavior
255: @ requires c != null
256: @ && (\forall Object o; c.contains(o);
257: @ o == null || (o instanceof JMLType));
258: @ requires c.size() < Integer.MAX_VALUE;
259: @ ensures \result != null && \result.int_size() == c.size()
260: @ && (\forall JMLType x; c.contains(x) <==> \result.has(x));
261: @ also
262: @ public exceptional_behavior
263: @ requires c != null
264: @ && (\exists Object o; c.contains(o);
265: @ o != null && !(o instanceof JMLType));
266: @ signals (ClassCastException);
267: @*/
268: public static/*@ pure @*//*@ non_null @*/
269: JMLValueSet convertFrom(/*@ non_null @*/java.util.Collection c)
270: throws ClassCastException {
271: /*@ non_null @*/JMLValueSet ret = EMPTY;
272: java.util.Iterator celems = c.iterator();
273: while (celems.hasNext()) {
274: Object o = celems.next();
275: if (o == null) {
276: ret = ret.insert(null);
277: } else {
278: ret = ret.insert((JMLType) o);
279: }
280: }
281: return ret;
282: }
283:
284: /** Return the set containing all the value in the
285: * given JMLCollection.
286: * @throws ClassCastException if some element in c is not an instance of
287: * JMLType.
288: */
289: /*@ public normal_behavior
290: @ requires c != null
291: @ && (c.elementType <: \type(JMLType));
292: @ ensures \result != null
293: @ && (\forall JMLType x; c.has(x) <==> \result.has(x));
294: @ also
295: @ public exceptional_behavior
296: @ requires c != null && (\exists Object o; c.has(o);
297: @ !(o instanceof JMLType));
298: @ signals (ClassCastException);
299: @*/
300: public static/*@ pure @*//*@ non_null @*/
301: JMLValueSet convertFrom(/*@ non_null @*/JMLCollection c)
302: throws ClassCastException {
303: /*@ non_null @*/JMLValueSet ret = EMPTY;
304: JMLIterator celems = c.iterator();
305: while (celems.hasNext()) {
306: Object o = celems.next();
307: if (o == null) {
308: ret = ret.insert(null);
309: } else {
310: ret = ret.insert((JMLType) o);
311: }
312: }
313: return ret;
314: }
315:
316: //**************************** Observers **********************************
317:
318: /** Is the argument ".equals" to one of the
319: * values in theSet.
320: */
321: /*@ also
322: @ public normal_behavior
323: @ requires elem != null;
324: @ also
325: @ public normal_behavior
326: @ requires elem == null;
327: @ also
328: @ public normal_behavior
329: @ requires isEmpty();
330: @ ensures ! \result ;
331: @*/
332: public/*@ pure @*/boolean has(JMLType elem) {
333: return the_list != null && the_list.has(elem);
334: }
335:
336: /** Tell whether, for each element in the given collection, there is a
337: * ".equals" element in this set.
338: * @param c the collection whose elements are sought.
339: * @see #isSuperset(JMLValueSet)
340: * @see #convertFrom(java.util.Collection)
341: */
342: /*@ public normal_behavior
343: @ requires c != null;
344: @ ensures \result <==> (\forall Object o; c.contains(o); this.has(o));
345: @*/
346: public boolean containsAll(/*@ non_null @*/java.util.Collection c) {
347: java.util.Iterator celems = c.iterator();
348: while (celems.hasNext()) {
349: Object o = celems.next();
350: if (!has(o)) {
351: return false;
352: }
353: }
354: return true;
355: }
356:
357: /*@ also
358: @ public normal_behavior
359: @ ensures \result <==>
360: @ s2 != null && s2 instanceof JMLValueSet
361: @ && (\forall JMLType e; ; this.has(e)
362: @ == ((JMLValueSet)s2).has(e));
363: @ ensures_redundantly \result ==>
364: @ s2 != null && s2 instanceof JMLValueSet
365: @ && containsNull == ((JMLValueSet)s2).containsNull;
366: @*/
367: public boolean equals(Object s2) {
368: return (s2 != null && s2 instanceof JMLValueSet)
369: && (size == ((JMLValueSet) s2).int_size())
370: && isSubset((JMLValueSet) s2);
371: }
372:
373: /** Return a hash code for this object.
374: */
375: public int hashCode() {
376: if (size == 0) {
377: return 0;
378: } else {
379: int hash = 0xffff;
380: JMLListValueNode walker = the_list;
381: while (walker != null) {
382: JMLType wv = walker.val;
383: if (wv != null) {
384: hash ^= wv.hashCode();
385: }
386: walker = walker.next;
387: }
388: return hash;
389: }
390: }
391:
392: /** Is the set empty.
393: * @see #int_size()
394: * @see #has(JMLType)
395: */
396: /*@ public normal_behavior
397: @ ensures \result == (\forall JMLType e; ; !this.has(e));
398: @ also
399: @ protected normal_behavior
400: @ ensures the_list == null <==> \result;
401: @*/
402: public/*@ pure @*/boolean isEmpty() {
403: return the_list == null;
404: }
405:
406: /** Tells the number of elements in the set.
407: */
408: /*@ also
409: @ public normal_behavior
410: @ ensures
411: @ (this.isEmpty() ==> \result == 0)
412: @ && (!this.isEmpty() ==>
413: @ (\exists JMLType e; this.has(e);
414: @ \result == 1 + (this.remove(e).int_size())) );
415: @*/
416: public/*@ pure @*/int int_size() {
417: return size;
418: }
419:
420: /** Tells whether this set is a subset of or equal to the argument.
421: * @see #isProperSubset(JMLValueSet)
422: * @see #isSuperset(JMLValueSet)
423: */
424: /*@ public normal_behavior
425: @ requires s2 != null;
426: @ ensures \result <==>
427: @ (\forall JMLType e; ; this.has(e) ==> s2.has(e));
428: @*/
429: public boolean isSubset(/*@ non_null @*/JMLValueSet s2) {
430: if (size > s2.int_size()) {
431: return false;
432: } else {
433: for (JMLListValueNode walker = the_list; walker != null; walker = walker.next) {
434: if (!s2.has(walker.val)) {
435: return false;
436: }
437: }
438: return true;
439: }
440: }
441:
442: /** Tells whether this set is a subset of but not equal to the
443: * argument.
444: * @see #isSubset(JMLValueSet)
445: * @see #isProperSuperset(JMLValueSet)
446: */
447: /*@ public normal_behavior
448: @ requires s2 != null;
449: @ ensures \result <==>
450: @ this.isSubset(s2) && !this.equals(s2);
451: @*/
452: public boolean isProperSubset(/*@ non_null @*/JMLValueSet s2) {
453: return size < s2.int_size() && isSubset(s2);
454: }
455:
456: /** Tells whether this set is a superset of or equal to the argument.
457: * @see #isProperSuperset(JMLValueSet)
458: * @see #isSubset(JMLValueSet)
459: * @see #containsAll(java.util.Collection)
460: */
461: /*@ public normal_behavior
462: @ requires s2 != null;
463: @ ensures \result == s2.isSubset(this);
464: @*/
465: public boolean isSuperset(/*@ non_null @*/JMLValueSet s2) {
466: return s2.isSubset(this );
467: }
468:
469: /** Tells whether this set is a superset of but not equal to the
470: * argument.
471: * @see #isSuperset(JMLValueSet)
472: * @see #isProperSubset(JMLValueSet)
473: */
474: /*@ public normal_behavior
475: @ requires s2 != null;
476: @ ensures \result == s2.isProperSubset(this);
477: @*/
478: public boolean isProperSuperset(/*@ non_null @*/JMLValueSet s2) {
479: return s2.isProperSubset(this );
480: }
481:
482: /** Return an arbitrary element of this.
483: * @exception JMLNoSuchElementException if this is empty.
484: * @see #isEmpty()
485: * @see #elements()
486: */
487: /*@ public normal_behavior
488: @ requires !isEmpty();
489: @ ensures (\exists JMLType e; this.has(e);
490: @ (\result == null ==> e == null)
491: @ && (\result != null ==> \result.equals(e)));
492: @ also
493: @ public exceptional_behavior
494: @ requires isEmpty();
495: @ signals (JMLNoSuchElementException);
496: @*/
497: public JMLType choose() throws JMLNoSuchElementException {
498: if (the_list != null) {
499: JMLType entry = the_list.val;
500: if (entry == null) {
501: return null;
502: } else {
503: Object o = entry.clone();
504: return (JMLType) o;
505: }
506: } else {
507: throw new JMLNoSuchElementException("Tried to .choose() "
508: + "with JMLValueSet empty");
509: }
510: }
511:
512: // ****************** building new JMLValueSets **************************
513:
514: /** Return a clone of this object. This method clones the
515: * elements of the set.
516: */
517: /*@ also
518: @ public normal_behavior
519: @ ensures \result != null
520: @ && \result instanceof JMLValueSet
521: @ && this.equals(\result);
522: @*/
523: public Object clone() {
524: if (the_list == null) {
525: return this ;
526: } else {
527: return new JMLValueSet((JMLListValueNode) the_list.clone(),
528: size);
529: }
530: }
531:
532: /** Returns a new set that contains all the elements of this and
533: * also the given argument.
534: * @see #has(JMLType)
535: * @see #remove(JMLType)
536: */
537: /*@ also
538: @ public normal_behavior
539: @ requires int_size() < Integer.MAX_VALUE || has(elem);
540: @ ensures \result != null
541: @ && (\forall JMLType e; ;
542: @ \result.has(e) <==> this.has(e)
543: @ || (e == null && elem == null)
544: @ || (e != null && e.equals(elem)));
545: @ ensures_redundantly this.isSubset(\result) && \result.has(elem)
546: @ && \result.int_size() == this.int_size() + (this.has(elem) ? 0 : 1);
547: @ also public normal_behavior
548: @ ensures elem == null ==> \result.containsNull;
549: @ ensures elem != null ==> \result.containsNull == containsNull;
550: @*/
551: public JMLValueSet insert(JMLType elem)
552: throws IllegalStateException {
553: if (has(elem)) {
554: return this ;
555: } else if (size < Integer.MAX_VALUE) {
556: return fast_insert(elem);
557: } else {
558: throw new IllegalStateException("Cannot insert into a set "
559: + "with Integer.MAX_VALUE elements");
560: }
561: }
562:
563: /** Returns a new set that contains all the elements of this and
564: * also the given argument, assuming the argument is not in the set.
565: * @see #insert(JMLType)
566: */
567: /*@ protected normal_behavior
568: @ requires !has(elem);
569: @ requires int_size() < Integer.MAX_VALUE;
570: @ ensures \result != null
571: @ && (\forall JMLType e; ;
572: @ \result.has(e) <==> this.has(e)
573: @ || (e == null && elem == null)
574: @ || (e != null && e.equals(elem)));
575: @ ensures_redundantly this.isSubset(\result) && \result.has(elem)
576: @ && \result.int_size() == this.int_size() + 1;
577: @*/
578: protected/*@ non_null @*/JMLValueSet fast_insert(JMLType elem) {
579: return new JMLValueSet( // cons() clones if necessary
580: JMLListValueNode.cons(elem, the_list), size + 1);
581: }
582:
583: /** Returns a new set that contains all the elements of this except for
584: * the given argument.
585: * @see #has(JMLType)
586: * @see #insert(JMLType)
587: */
588: /*@ public normal_behavior
589: @ ensures \result != null
590: @ && (\forall JMLType e; ;
591: @ \result.has(e) <==>
592: @ this.has(e) && !((e == null && elem == null)
593: @ || (e != null && e.equals(elem))));
594: @ ensures_redundantly \result.isSubset(this) && !\result.has(elem)
595: @ && \result.int_size() == this.int_size() - (this.has(elem) ? 1 : 0);
596: @*/
597: public/*@ non_null @*/JMLValueSet remove(JMLType elem) {
598: if (!has(elem)) {
599: return this ;
600: } else {
601: JMLListValueNode new_list = the_list.remove(elem);
602: return new JMLValueSet(new_list, size - 1);
603: }
604: }
605:
606: /** Returns a new set that contains all the elements that are in
607: * both this and the given argument.
608: * @see #union(JMLValueSet)
609: * @see #difference(JMLValueSet)
610: */
611: /*@ public normal_behavior
612: @ requires s2 != null;
613: @ ensures \result != null
614: @ && (\forall JMLType e; ;
615: @ \result.has(e) <==> this.has(e) && s2.has(e));
616: @*/
617: public/*@ non_null @*/
618: JMLValueSet intersection(/*@ non_null @*/JMLValueSet s2) {
619: JMLValueSet returnSet = new JMLValueSet();
620: JMLListValueNode this Walker = the_list;
621: while (this Walker != null) {
622: if (s2.has(this Walker.val)) {
623: returnSet = returnSet.fast_insert(this Walker.val);
624: }
625: this Walker = this Walker.next;
626: }
627: return returnSet;
628: }
629:
630: /*@ public normal_behavior
631: @ requires s2 != null;
632: @ requires int_size() < Integer.MAX_VALUE - s2.difference(this).int_size();
633: @ ensures \result != null
634: @ && (\forall JMLType e; ;
635: @ \result.has(e) <==> this.has(e) || s2.has(e));
636: @*/
637: public/*@ non_null @*/
638: JMLValueSet union(/*@ non_null @*/JMLValueSet s2)
639: throws IllegalStateException {
640: JMLValueSet returnSet = s2;
641: JMLListValueNode this Walker = the_list;
642: while (this Walker != null) {
643: returnSet = returnSet.insert(this Walker.val);
644: this Walker = this Walker.next;
645: }
646: return returnSet;
647: }
648:
649: /*@ public normal_behavior
650: @ requires s2 != null;
651: @ ensures \result != null
652: @ && (\forall JMLType e; ;
653: @ \result.has(e) <==> this.has(e) && !s2.has(e));
654: @*/
655: public/*@ non_null @*/
656: JMLValueSet difference(/*@ non_null @*/JMLValueSet s2) {
657: JMLValueSet returnSet = new JMLValueSet();
658: JMLListValueNode this Walker = the_list;
659: while (this Walker != null) {
660: if (!s2.has(this Walker.val)) {
661: returnSet = returnSet.fast_insert(this Walker.val);
662: }
663: this Walker = this Walker.next;
664: }
665: return returnSet;
666: }
667:
668: /*@ public normal_behavior
669: @ requires int_size() < 32;
670: @ ensures \result != null
671: @ && (\forall JMLValueSet s; ;
672: @ s.isSubset(this) <==> \result.has(s));
673: @ ensures_redundantly \result != null
674: @ && (0 < size && size <= 31
675: @ ==> \result.int_size() == (2 << (int_size()-1)));
676: @*/
677: public/*@ non_null @*/JMLValueSet powerSet()
678: throws IllegalStateException {
679: if (size >= 32) {
680: throw new IllegalStateException(
681: "Can't compute the powerSet "
682: + "of such a large set");
683: }
684:
685: // This a dynamic programming algorithm.
686: /*@ non_null @*/JMLValueSet ret = new JMLValueSet(EMPTY);
687:
688: //@ loop_invariant !ret.containsNull;
689: /*@ maintaining 0 <= i && i <= int_size() && ret.size >= 1
690: @ && (\forall JMLValueSet s; s.int_size() <= i;
691: @ s.isSubset(this) <==> ret.has(s));
692: @ decreasing int_size()-i;
693: @*/
694: for (int i = 0; i < int_size(); i++) {
695: Enumeration size_i_and_smaller_subsets = ret.elements();
696: while (size_i_and_smaller_subsets.hasMoreElements()) {
697: // System.out.println("In middle loop, ret == " + ret);
698: Object s = size_i_and_smaller_subsets.nextElement();
699: JMLValueSet subset = (JMLValueSet) s;
700: Enumeration elems = elements();
701: while (elems.hasMoreElements()) {
702: Object o = elems.nextElement();
703: // System.out.println(this + ".powerSet() inserting " + o);
704: if (o == null) {
705: ret = ret.insert(subset.insert(null));
706: } else {
707: ret = ret.insert(subset.insert((JMLType) o));
708: }
709: }
710: }
711: }
712: return ret;
713: }
714:
715: /** Return a new JMLValueBag containing all the elements of this.
716: * @see #toSequence()
717: */
718: /*@ public normal_behavior
719: @ ensures \result != null
720: @ && (\forall JMLType o;;
721: @ \result.count(o) == 1 <==> this.has(o));
722: @*/
723: public /*@ non_null @*/ JMLValueBag toBag() {
724: JMLValueBag ret = new JMLValueBag();
725: JMLValueSetEnumerator enum = elements();
726: while (enum.hasMoreElements()) {
727: Object o = enum.nextElement();
728: JMLType e = (o == null ? null : (JMLType) o);
729: ret = ret.insert(e);
730: }
731: return ret;
732: }
733: /** Return a new JMLValueSequence containing all the elements of this.
734: * @see #toBag()
735: * @see #toArray()
736: */
737: /*@ public normal_behavior
738: @ ensures \result != null
739: @ && (\forall JMLType o;;
740: @ \result.count(o) == 1 <==> this.has(o));
741: @*/
742: public /*@ non_null @*/ JMLValueSequence toSequence() {
743: JMLValueSequence ret = new JMLValueSequence();
744: JMLValueSetEnumerator enum = elements();
745: while (enum.hasMoreElements()) {
746: Object o = enum.nextElement();
747: JMLType e = (o == null ? null : (JMLType) o);
748: ret = ret.insertFront(e);
749: }
750: return ret;
751: }
752: /** Return a new array containing all the elements of this.
753: * @see #toSequence()
754: */
755: /*@ public normal_behavior
756: @ ensures \result != null && \result.length == int_size()
757: @ && (\forall JMLType o;;
758: @ JMLArrayOps.hasValueEquals(\result, o) <==> has(o));
759: @ ensures_redundantly \result != null && \result.length == int_size()
760: @ && (\forall int i; 0 <= i && i < \result.length;
761: @ JMLArrayOps.hasValueEquals(\result, \result[i])
762: @ == has(\result[i]));
763: @*/
764: public /*@ non_null @*/ JMLType[] toArray() {
765: JMLType[] ret = new JMLType[int_size()];
766: JMLValueSetEnumerator enum = elements();
767: int i = 0;
768: //@ loop_invariant 0 <= i && i <= ret.length;
769: while (enum.hasMoreElements()) {
770: Object o = enum.nextElement();
771: if (o == null) {
772: ret[i] = null;
773: } else {
774: JMLType e = (JMLType) o;
775: ret[i] = (JMLType) e.clone();
776: }
777: i++;
778: }
779: return ret;
780: }
781: //********************** Tools Methods *********************************
782: // The elements and toString methods are of no value for writing
783: // assertions in JML. They are included for the use of developers
784: // of CASE tools based on JML, e.g., type checkers, assertion
785: // evaluators, prototype generators, test tools, ... . They can
786: // also be used in model programs in specifications.
787:
788: /** Returns an Enumeration over this set.
789: * @see #iterator()
790: */
791: /*@ public normal_behavior
792: @ ensures \fresh(\result) && this.equals(\result.uniteratedElems);
793: @*/
794: public/*@ non_null @*/JMLValueSetEnumerator elements() {
795: return new JMLValueSetEnumerator(this );
796: }
797:
798: /** Returns an Iterator over this set.
799: * @see #elements()
800: */
801: /*@ also
802: @ public normal_behavior
803: @ ensures \fresh(\result)
804: @ && \result.equals(new JMLEnumerationToIterator(elements()));
805: @*/
806: public JMLIterator iterator() {
807: return new JMLEnumerationToIterator(elements());
808: }
809:
810: public String toString() {
811: String newStr = new String("{");
812: JMLListValueNode setWalker = the_list;
813: if (setWalker != null) {
814: newStr = newStr + setWalker.val;
815: setWalker = setWalker.next;
816: }
817: while (setWalker != null) {
818: newStr = newStr + ", " + setWalker.val;
819: setWalker = setWalker.next;
820: }
821: newStr = newStr + "}";
822: return newStr;
823: }
824:
825: }
|