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