001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package javafe.util; 004 005 import java.util.Vector; 006 007 /** 008 * A stack of Vector objects. 009 * 010 * <p> Contains 1 or more Vectors arranged in a stack. Direct access 011 * is allowed only to the elements of the top Vector via a subset of 012 * the usual java.util.Vector operations. These Vectors may not 013 * contain null elements.<p> 014 * 015 * <p> push() pushs a zero-length Vector on the stack, pop() discards 016 * the top Vector, and merge() combines the top two Vectors. 017 * 018 * <p> The caller is responsible for ensuring that pop() and merge() 019 * are called only when the stack has at least 2 Vectors on it. 020 * 021 * <p> All the elements in the Vectors must be of type elementType. 022 * 023 * <p> Note: Although this class as a whole is thread safe, individual 024 * instances are not. Thus, different threads can safely access 025 * different instances of <CODE>StackVector</CODE> without any 026 * synchronization, but different threads accessing the <EM>same</EM> 027 * instance will have to lock and synchronize. 028 */ 029 030 public final class StackVector 031 { 032 /*************************************************** 033 * * 034 * Private instance fields: * 035 * * 036 **************************************************/ 037 038 /** The type of our elements */ 039 //@ ghost public \TYPE elementType; 040 041 /** 042 * Our data representation is as follows: <p> 043 * 044 * elements[0], ..., elements[elementCount-1] contain 045 * the Vectors on our stack, stored as sequences of elements from 046 * the bottom of the stack (pushed longest ago) to the top of the 047 * stack. Each sequence is seperated by a null element.<p> 048 * 049 * Example: [1, 2, null, 3, 4, null, 5, 6] represents the stack [1, 050 * 2], [3, 4], [5, 6] where the Vector [5, 6] is on top so 051 * elementAt(1) will return 6. <p> 052 * 053 * To speed access to the top Vector, currentStackBottom points to 054 * the first element of the top Vector (5 in the example). Note 055 * that this may point just beyond the last element of elements if 056 * the top Vector is zero-length.<p> 057 * 058 * vectorCount holds the # of Vectors; it exists so that clients 059 * can make sure they've left a StackVector the way they found it 060 * and so that preconditions can be written for pop(), etc.<p> 061 */ 062 063 //@ invariant elements != null; 064 //@ invariant elements.length>0; 065 //@ invariant \typeof(elements) == \type(Object[]); 066 067 //@ invariant elements.owner == this; 068 private /*@ spec_public */ Object[] elements = new Object[10]; 069 070 071 //@ invariant 0<=elementCount && elementCount <= elements.length; 072 /*@ invariant (\forall int i; 0<=i && i<elementCount 073 ==> elements[i]==null || \typeof(elements[i]) <: elementType); */ 074 075 /*@spec_public*/ private int elementCount = 0; 076 077 078 //@ invariant 0<=currentStackBottom && currentStackBottom<=elementCount; 079 080 /*@ invariant currentStackBottom == 0 || 081 elements[currentStackBottom-1]==null; */ 082 083 /*@spec_public*/ private int currentStackBottom = 0; 084 085 086 //@ invariant vectorCount>=1; 087 /* 088 * The following invariant is used in the form of assumes as needed, 089 * but not checked. (too hard) 090 * 091 * (vectorCount>=2) ==> (currentStackBottom>0) 092 */ 093 /*@spec_public*/ private int vectorCount = 1; 094 095 096 /*************************************************** 097 * * 098 * Constructors: * 099 * * 100 **************************************************/ 101 102 /** 103 * Create a StackVector that contains only 1 zero-length Vector. 104 */ 105 //@ ensures elementCount == 0; 106 //@ ensures vectorCount == 1; 107 public StackVector() { 108 //@ set elements.owner = this; 109 } 110 111 112 /*************************************************** 113 * * 114 * Accessing the top Vector: * 115 * * 116 **************************************************/ 117 118 /** 119 * Return the size of the top Vector. <p> 120 * 121 * Indices into the top Vector range from 0 to size()-1.<p> 122 * 123 */ 124 //@ ensures \result >= 0 ; 125 //@ ensures \result == (elementCount - currentStackBottom); 126 //@ pure 127 public final int size() { 128 return elementCount - currentStackBottom; 129 } 130 131 132 /* 133 * Precondition is for the default case where caller does not want 134 * ArrayIndexOutOfBoundsException raised. 135 * 136 * If caller does want to deal with this, use nowarn Pre on calls to 137 * these functions. 138 */ 139 //@ requires 0<=index && index+currentStackBottom<elementCount; 140 private void checkBounds(int index) 141 /*throws ArrayIndexOutOfBoundsException*/ { 142 if (index < 0 || index+currentStackBottom >= elementCount) { 143 throw new ArrayIndexOutOfBoundsException(index); 144 } 145 } 146 147 /** 148 * Return the element in the top Vector at the given index. <p> 149 * 150 * @exception ArrayIndexOutOfBoundsException if the index is out of 151 * range. 152 */ 153 //@ requires 0<=i && i+currentStackBottom<elementCount; 154 //@ ensures \typeof(\result) <: elementType; 155 //@ ensures \result != null; 156 public Object elementAt(int i) 157 /*throws ArrayIndexOutOfBoundsException*/ { 158 checkBounds(i); 159 return elements[currentStackBottom + i]; 160 } //@ nowarn Post; // (thinks could be null) 161 162 public void setElementAt(Object o, int i) 163 /*throws ArrayIndexOutOfBoundsException*/ { 164 checkBounds(i); 165 elements[currentStackBottom + i] = o; 166 } 167 168 /** 169 * Add x to the end of the top Vector. <p> 170 * 171 * x may be null, in which case the caller needs to cleanup to 172 * ensure that a null element does not stay in the top Vector. <p> 173 */ 174 //@ requires x==null || \typeof(x) <: elementType; 175 //@ modifies elementCount, elements; 176 //@ ensures elementCount == \old(elementCount)+1; 177 //@ ensures elementCount>0 && elements[elementCount-1]==x; 178 private void addElementInternal(Object x) { 179 if (elementCount >= elements.length) { 180 Object[] newElements = new Object[2*elementCount]; 181 //@ set newElements.owner = this; 182 183 System.arraycopy(elements, 0, newElements, 0, elements.length); 184 elements = newElements; 185 } 186 187 elements[elementCount++] = x; 188 } 189 190 191 /** 192 * Add an element at the end of the top Vector. <p> 193 * 194 */ 195 //@ requires x != null; 196 //@ requires \typeof(x) <: elementType; 197 //@ modifies elementCount, elements; 198 /*@ ensures (elementCount - currentStackBottom) == 199 (\old(elementCount) - currentStackBottom) + 1; */ 200 public final void addElement(Object x) { 201 Assert.precondition(x != null); 202 203 addElementInternal(x); 204 } 205 206 207 /* 208 public final void addElements(Enumeration e) { 209 while( e.hasMoreElements() ) 210 addElement( e.nextElement() ); 211 } 212 */ 213 214 215 /** Zero the top Vector. */ 216 //@ modifies elementCount; 217 //@ ensures elementCount == currentStackBottom; 218 public final void removeAllElements() { 219 for (int i = currentStackBottom; i < elementCount; i++) 220 elements[i] = null; // Allow for GC 221 elementCount = currentStackBottom; 222 } 223 224 225 //@ requires dst != null; 226 //@ requires (elementCount - currentStackBottom) <= dst.length; 227 //@ modifies dst[*]; 228 /*@ ensures (\forall int i; 0 <= i && i < elementCount-currentStackBottom 229 ==> dst[i] != null); */ 230 public final void copyInto(Object[] dst) { 231 System.arraycopy(elements, currentStackBottom, 232 dst, 0, 233 elementCount - currentStackBottom); 234 } //@ nowarn Post; 235 236 237 /** 238 * Return true iff the top Vector contains o. 239 */ 240 public final boolean contains(Object o) { 241 for( int i=currentStackBottom; i<elementCount; i++ ) { 242 if( elements[i] == o ) return true; 243 } 244 return false; 245 } 246 247 248 /*************************************************** 249 * * 250 * Stack manipulation methods: * 251 * * 252 **************************************************/ 253 254 /** 255 * Reset us to the state where we contain only 1 Vector, which has 256 * zero-length. 257 */ 258 //@ modifies vectorCount; 259 //@ ensures vectorCount == 1; 260 //@ modifies elementCount, currentStackBottom; 261 //@ ensures elementCount == 0; 262 //@ ensures currentStackBottom == 0; 263 public void clear() { 264 elementCount = currentStackBottom = 0; 265 vectorCount = 1; 266 } 267 268 269 /** 270 * Return the number of Vectors on our stack. <p> 271 * 272 */ 273 //@ ensures \result==vectorCount; 274 public final int vectors() { 275 return vectorCount; 276 } 277 278 279 /** 280 * Push a zero-length Vector. 281 * 282 */ 283 //@ modifies vectorCount, currentStackBottom, elementCount, elements; 284 //@ ensures vectorCount == \old(vectorCount)+1; 285 //@ ensures currentStackBottom == elementCount; 286 public void push() { 287 addElementInternal(null); 288 currentStackBottom = elementCount; 289 vectorCount++; 290 } 291 292 /** 293 * Pop off the current top Vector. <p> 294 * 295 * Precondition: at least 2 Vectors are on our stack.<p> 296 */ 297 //@ requires vectorCount>=2; 298 //@ modifies vectorCount; 299 //@ ensures vectorCount == \old(vectorCount)-1; 300 //@ modifies elementCount, currentStackBottom; 301 public void pop() { 302 //@ assume (vectorCount>=2) ==> (currentStackBottom>0); // "invariant" 303 304 Assert.precondition(currentStackBottom>0); 305 306 int i = currentStackBottom - 1; 307 //@ assert elements[i]==null; 308 309 elementCount = i; 310 for( ; i > 0; i--) 311 if (elements[i-1] == null) 312 break; 313 currentStackBottom = i; 314 315 vectorCount--; 316 } 317 318 319 /** 320 * Merge the top Vector with the Vector just under it by appending 321 * the former to the latter. <p> 322 * 323 * Example: ..., A, TOP -> ..., A^TOP <p> 324 * 325 * Precondition: there are at least two vectors on our stack.<p> 326 */ 327 //@ requires vectorCount>=2; 328 //@ modifies vectorCount, elementCount; 329 //@ ensures vectorCount == \old(vectorCount)-1; 330 //@ modifies currentStackBottom; 331 public void merge() { 332 //@ assume (vectorCount>=2) ==> (currentStackBottom>0); // "invariant" 333 334 Assert.precondition(currentStackBottom>0); 335 336 int i = currentStackBottom - 1; 337 //@ assert elements[i]==null; 338 339 System.arraycopy(elements, i+1, elements, i, size()); 340 for( ; i > 0; i--) 341 if (elements[i - 1] == null) 342 break; 343 currentStackBottom = i; 344 elementCount--; 345 346 vectorCount--; 347 } 348 349 /** 350 ** Returns the contents of all the vectors on the stack as a single 351 ** vector.<p> 352 **/ 353 public Vector stackContents() { 354 Vector vec = new Vector(); 355 for (int i = 0; i < elementCount; i++) { 356 Object o = elements[i]; 357 if (o != null) { 358 vec.addElement(o); 359 } 360 } 361 return vec; 362 } 363 364 public String toString() { 365 StringBuffer sb = new StringBuffer(); 366 sb.append("StackVector["); 367 for (int i=0; i<elementCount; ++i) { 368 Object o = elements[i]; 369 if (o==null) sb.append(" :: "); 370 else { 371 sb.append(o.toString()); 372 sb.append(" "); 373 } 374 } 375 sb.append("]"); 376 return sb.toString(); 377 } 378 379 }