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 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    }