    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    }