    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    }