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