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    }