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 }