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 /*@non_null*/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 }