001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package javafe.util;
004
005 import java.util.*;
006
007 /**
008 * A simple implementation of imperative sets. Set's may not contain
009 * null.
010 */
011
012 public class Set implements Cloneable
013 {
014 /***************************************************
015 * *
016 * Instance variables: *
017 * *
018 **************************************************/
019
020 /** Our element type */
021 //@ ghost public \TYPE elementType;
022
023
024 /**
025 * We contain the element e iff ht has the mapping e -> e. <p>
026 *
027 * All mappings of ht are of the form e' -> e' for some e'.
028 */
029 //+@ invariant ht.keyType == elementType;
030 //+@ invariant ht.elementType == elementType;
031 //@ invariant ht.owner == this;
032 //@ spec_public
033 private /*@ non_null @*/ Hashtable ht;
034
035
036 /***************************************************
037 * *
038 * Construction: *
039 * *
040 **************************************************/
041
042 /**
043 * Create an empty set
044 */
045 public Set() {
046 int initCapacity = 5;
047 ht = new Hashtable(initCapacity);
048 //+@ set ht.keyType = elementType;
049 //+@ set ht.elementType = elementType;
050 //@ set ht.owner = this;
051 }
052
053
054 /**
055 * Create a set from the elements of an Enumeration
056 */
057 //@ requires e != null;
058 //@ requires !e.returnsNull;
059 //@ ensures elementType == e.elementType;
060 public Set(Enumeration e) {
061 this();
062 //@ set elementType = e.elementType;
063 //+@ set ht.keyType = e.elementType;
064 //+@ set ht.elementType = e.elementType;
065
066 while( e.hasMoreElements() ) {
067 Object item = e.nextElement();
068 Assert.notNull(item);
069 add( item );
070 }
071 }
072
073
074 /***************************************************
075 * *
076 * Inspectors: *
077 * *
078 **************************************************/
079
080 /**
081 * Return the number of elements we hold.
082 */
083 public int size() {
084 return ht.size();
085 }
086
087 /**
088 * Do we contain no elements?
089 */
090 public boolean isEmpty() {
091 return ht.isEmpty();
092 }
093
094
095 /**
096 * Do we contain a particular element?
097 */
098 //@ requires o != null;
099 //@ requires \typeof(o) <: elementType;
100 public boolean contains(Object o) {
101 return ht.containsKey( o );
102 }
103
104
105 /**
106 * Return an enumeration of our elements
107 */
108 //@ ensures \result != null;
109 //@ ensures !\result.returnsNull;
110 //@ ensures \result.elementType == elementType;
111 public Enumeration elements() {
112 return ht.keys();
113 }
114
115
116 public /*@non_null*/String toString() {
117 return "[SET: "+ht.toString()+"]";
118 }
119
120
121 /***************************************************
122 * *
123 * Manipulators: *
124 * *
125 **************************************************/
126
127 /**
128 * Remove all our elements
129 */
130 public void clear() {
131 ht.clear();
132 }
133
134
135 /**
136 * Add an element
137 *
138 * Return 'true' iff the element was already in the set.
139 */
140 //@ requires o != null;
141 //@ requires \typeof(o) <: elementType;
142 public boolean add(Object o) {
143 return ht.put( o, o ) != null;
144 }
145
146 /**
147 * Add all the elements of a given enumeration
148 */
149 //@ requires e != null;
150 //@ requires !e.returnsNull;
151 //@ requires e.elementType <: elementType;
152 public void addEnumeration(Enumeration e) {
153 while( e.hasMoreElements() ) {
154 Object item = e.nextElement();
155 Assert.notNull(item);
156 add( item );
157 }
158 }
159
160
161 /**
162 * Remove a particular element if we contain it. Return true
163 * iff the element was previously in the set.
164 */
165 //@ requires o != null;
166 //@ requires \typeof(o) <: elementType;
167 public boolean remove(Object o) {
168 return ht.remove(o) != null;
169 }
170
171
172 /**
173 * Remove all elements not contained in another set. This has the
174 * effect of setting us to the intersection of our original value
175 * and the other set.
176 */
177 //@ requires s != null;
178 //@ requires s.elementType == elementType;
179 public void intersect(Set s) {
180 Enumeration e = ht.keys();
181 while( e.hasMoreElements() ) {
182 Object o = e.nextElement();
183 if (!s.ht.containsKey(o))
184 ht.remove(o);
185 }
186 }
187
188
189 /**
190 * Adds all elements in another set. This has the
191 * effect of setting us to the union of our original value
192 * and the other set. Return true if any values were added.
193 */
194 //@ requires s != null;
195 //@ requires s.elementType == elementType;
196 public boolean union(Set s) {
197 boolean changed = false;
198 for(Enumeration e = s.elements(); e.hasMoreElements(); ) {
199 Object o = e.nextElement();
200 if (!ht.containsKey(o)) {
201 changed = true;
202 ht.put(o,o);
203 }
204 }
205 return changed;
206 }
207
208 /**
209 * Returns whether or not the set has any element in common with
210 * <code>s</code>. Thus, if the intersection of the sets is empty,
211 * that is, if the sets are disjoint, then <code>false</code> is returned.
212 * The operation leaves both sets unchanged.
213 */
214 //@ requires s != null;
215 //@ requires s.elementType == elementType;
216 public boolean containsAny(Set s) {
217 Enumeration e;
218 if (size() < s.size()) {
219 e = ht.keys();
220 } else {
221 e = s.ht.keys();
222 s = this;
223 }
224 while (e.hasMoreElements()) {
225 Object o = e.nextElement();
226 if (s.ht.containsKey(o)) {
227 return true;
228 }
229 }
230 return false;
231 }
232
233 public Object clone() {
234 try {
235 Set s = (Set)super.clone();
236 //@ assume s.elementType == this.elementType;
237 Enumeration e = this.elements();
238 s.addEnumeration(e);
239 return s;
240 } catch (CloneNotSupportedException c) {
241 // shouldn't happen, since Set implements Cloneable
242 //@ unreachable; //@ nowarn;
243 Assert.fail("unexpected CloneNotSupportedException exception");
244 return null; // satisfy compiler
245 }
246 }
247
248 }