    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    /*
    004     * File: VarInitVec.java <p>
    005     *
    006     * This file is a template for a vector of X.  It is filled in using
    007     * sed (e.g, see the Makefile for javafe.ast).  The following
    008     * replacements need to be done:<p>
    009     *
    010     * VarInit should be globally replaced with the simple name of the
    011     *              element type<p>
    012     * javafe.ast should be globally replaced with the package the resulting
    013     *              Vector type should live in<p>
    014     * javafe.ast should be globally replaced with the package the
    015     *              element type belongs to<p>
    016     *
    017     * The resulting type will have name VarInitVec.<p>
    018     *
    019     * Example: to make a vector of java.lang.Integer's that lives in
    020     * javafe.ast, substitute Integer, javafe.ast, and java.lang
    021     * respectively.<p>
    022     *
    023     *
    024     * By Default, VarInitVec's may not contain nulls.  If the ability to
    025     * hold nulls is desired, remove all lines with "// @@@@" on them.<p>
    026     */
    027
    028
    029
    030
    031    /**
    032     ** VarInitVec: A Vector of VarInit's. <p>
    033     **
    034     ** The interface to this class follows java.util.Vector, where
    035     ** appropriate. <p>
    036     **
    037     **
    038     ** This class was automatically created from the template
    039     ** javafe.util/_<tt>TYPE</tt>_Vec.j.<p>
    040     **
    041     ** DO NOT EDIT!!<p>
    042     **/
    043
    044    package javafe.ast;
    045
    046
    047    import java.util.Vector;
    048    import javafe.util.StackVector;
    049
    050    import javafe.ast.VarInit;
    051
    052
    053    public class  VarInitVec {
    054
    055        /***************************************************
    056         *                                                 *
    057         * Instance fields:                                *
    058         *                                                 *
    059         ***************************************************/
    060
    061        private /*@ spec_public non_null*/ VarInit[] elements;
    062        //@ invariant (\forall int i; (0<=i && i<count) ==> elements[i]!=null);
    063        //@ invariant \typeof(elements) == \type(VarInit[]);
    064
    065        //@ invariant elements.owner == this;
    066
    067        /*@spec_public*/ private int count;
    068        //@ invariant 0 <= count;
    069        //@ invariant count <= elements.length;
    070
    071
    072        /***************************************************
    073         *                                                 *
    074         * Private constructors:                           *
    075         *                                                 *
    076         ***************************************************/
    077
    078        //@ requires els!=null;
    079        //@ requires \nonnullelements(els);                         // @@@@
    080        //@ ensures count == els.length;
    081        //@ pure
    082        private VarInitVec(VarInit[] els) {
    083            this.count = els.length;
    084            this.elements = new VarInit[count];
    085            //@ set elements.owner = this;
    086
    087            System.arraycopy(els,0, elements,0, count);
    088        }
    089
    090        //@ requires cnt >= 0;
    091        //@ ensures this.elements.length >= cnt;
    092        //@ pure
    093        private VarInitVec(int cnt) {
    094            this.elements = new VarInit[(cnt == 0 ? 2 : cnt)];
    095            //@ set elements.owner = this;
    096
    097            this.count = 0;
    098        }
    099
    100
    101        /***************************************************
    102         *                                                 *
    103         * Public maker methods:                           *
    104         *                                                 *
    105         ***************************************************/
    106
    107        //@ ensures \result!=null;
    108        //@ ensures \fresh(\result);
    109        //@ pure
    110        public static VarInitVec make() {
    111            return new VarInitVec(0);
    112        }
    113
    114        //@ requires count >= 0;
    115        //@ ensures \result!=null;
    116        //@ ensures \fresh(\result);
    117        public static VarInitVec make(int count) {
    118            return new VarInitVec(count);
    119        }
    120
    121        //@ requires vec!=null;
    122        //@ requires vec.elementType <: \type(VarInit);
    123        //@ requires !vec.containsNull;
    124        //@ ensures \result!=null;
    125        //@ ensures \fresh(\result);
    126        public static VarInitVec make(Vector vec) {
    127            int sz = vec.size();
    128            VarInitVec result = new VarInitVec(sz);
    129            result.count = sz;
    130            vec.copyInto(result.elements);
    131            return result;
    132        }
    133
    134        //@ requires els!=null;
    135        //@ requires \nonnullelements(els);
    136        //@ ensures \result!=null;
    137        //@ ensures \result.count == els.length;
    138        //@ ensures \fresh(\result);
    139        public static VarInitVec make(VarInit[] els) {
    140            return new VarInitVec(els);
    141        }
    142
    143        //
    144        //@ requires s.vectorCount>1;
    145        //@ requires s.elementType <: \type(VarInit);
    146        //@ ensures \result!=null;
    147        //@ ensures \result.count == (\old(s.elementCount) - \old(s.currentStackBottom));
    148        // These are from pop() on s:
    149        //@ modifies s.vectorCount;
    150        //@ ensures s.vectorCount == \old(s.vectorCount)-1;
    151        //@ modifies s.elementCount, s.currentStackBottom;
    152        public static VarInitVec popFromStackVector(/*@non_null*/ StackVector s) {
    153            // Creates a new VarInitVec from top stuff in StackVector
    154            int sz = s.size();
    155            VarInitVec r = new VarInitVec(sz);
    156            s.copyInto(r.elements);
    157            r.count = sz;
    158            s.pop();
    159            return r;
    160        }
    161
    162
    163        /***************************************************
    164         *                                                 *
    165         * Other methods:                                  *
    166         *                                                 *
    167         ***************************************************/
    168
    169        //@ requires 0<=index && index<count;
    170        //@ ensures \result!=null;                                  // @@@@
    171        //@ pure
    172        public final VarInit elementAt(int index)
    173              /*throws ArrayIndexOutOfBoundsException*/ {
    174            if (index < 0 || index >= count)
    175                throw new ArrayIndexOutOfBoundsException(index);
    176
    177            javafe.util.Assert.notNull(elements[index]);            // @@@@
    178            return elements[index];
    179        }
    180
    181        //@ requires 0<=index && index<count;
    182        //@ requires x!=null;                                       // @@@@
    183        public final void setElementAt(VarInit x, int  index)
    184            /*throws ArrayIndexOutOfBoundsException*/ {
    185            if (index < 0 || index >= count)
    186                throw new ArrayIndexOutOfBoundsException(index);
    187            elements[index] = x;
    188        }
    189
    190        //@ ensures \result==count;
    191        //@ pure
    192        public final int size() { return count; }
    193
    194        //@ pure
    195        public final String toString() {
    196            StringBuffer b = new StringBuffer();
    197            b.append("{VarInitVec");
    198            for(int i = 0; i < count; i++) {
    199                b.append(" ");
    200                if (elements[i]==null)
    201                    b.append("null");
    202                else
    203                    b.append(elements[i].toString());
    204            }
    205            b.append('}');
    206            return b.toString();
    207        }
    208
    209      //@ ensures \result!=null;
    210      //@ ensures \nonnullelements(\result);                        // @@@@
    211      //@ pure
    212      public final VarInit[] toArray() {
    213          int ct = count;
    214          VarInit[] b = new VarInit[ ct ];
    215          for(int i = 0; i < ct; i++) {
    216              b[i]=elements[i];
    217          }
    218          return b;
    219      }
    220
    221      //@ ensures \result!=null;
    222      //@ pure
    223      public final VarInitVec copy() {
    224        VarInitVec result = new VarInitVec(count);
    225        result.count = count;
    226        System.arraycopy(elements,0,result.elements,0,count);
    227        return result;
    228      }
    229
    230      //@ requires x!=null;                                         // @@@@
    231      public boolean contains(VarInit x) {
    232        for(int i = 0; i < count; i++) {
    233          if( elements[i] == x ) return true;
    234        }
    235        return false;
    236      }
    237
    238      //@ requires x!=null;                                         // @@@@
    239      //@ modifies count,elements;
    240      //@ ensures count==\old(count)+1;
    241      public final void addElement(VarInit x) {
    242        if( count == elements.length ) {
    243          VarInit[] newElements = new VarInit[ 2*(elements.length==0 ?
    244                                                  2 : elements.length) ];
    245          //@ set newElements.owner = this;
    246
    247          System.arraycopy(elements, 0, newElements, 0, elements.length );
    248          elements = newElements;
    249        }
    250        elements[count++]=x;
    251      }
    252
    253      //@ requires x!=null;                                         // @@@@
    254      //@ modifies count;
    255      public final boolean removeElement(VarInit x) {
    256        for( int i=0; i<count; i++ ) {
    257          if( elements[i] == x ) {
    258              int ct=count;
    259            for( int j=i+1; j<ct; j++ )
    260              elements[j-1]=elements[j];
    261            count--;
    262            return true;
    263          }
    264        }
    265        return false;
    266      }
    267
    268        //@ requires 0<=i && i<count;
    269        //@ modifies count;
    270        public final void removeElementAt(int i) {
    271            int ct=count;
    272            for (int j=i+1; j<ct; j++) {
    273                elements[j-1]=elements[j];
    274            }
    275            count--;
    276        }
    277
    278        //@ requires count>0;
    279        //@ modifies count;
    280        //@ ensures count==\old(count)-1;
    281        //@ ensures \result!=null;
    282        public final VarInit pop() {
    283            count--;
    284            VarInit result = elements[count];
    285            elements[count] = null;
    286            return result;
    287        }
    288
    289
    290        //@ modifies count;
    291        //@ ensures count==0;
    292        public final void removeAllElements() {
    293            count = 0;
    294        }
    295
    296
    297      //@ requires 0 <= index && index <= this.count;
    298      //@ requires obj!=null;
    299      //@ modifies count,elements;
    300      //@ ensures count==\old(count)+1;
    301      public final void insertElementAt(VarInit obj, int index) {
    302        if( count == elements.length ) {
    303          VarInit[] newElements = new VarInit[ 2*(elements.length==0 ?
    304                                                  2 : elements.length) ];
    305          //@ set newElements.owner = this;
    306          System.arraycopy(elements, 0, newElements, 0, elements.length );
    307          elements = newElements;
    308        }
    309        int ct=count;
    310        //-@ loop_predicate i!=ct ==> elements[ct] != null, i<= ct; // FIXME - what are the semantics
    311        for( int i=count; i>index; i--)
    312          elements[i]=elements[i-1];
    313        elements[index]=obj;
    314        count++;
    315      }
    316
    317      //@ requires vec!=null;
    318      //@ modifies count,elements;
    319      //@ ensures count==\old(count)+vec.count;
    320      public final void append(VarInitVec vec) {
    321          //-@ loop_predicate count == \old(count)+i, i <= vec.count; // FIXME - what are the semantics
    322        for( int i=0; i<vec.size(); i++)
    323          addElement( vec.elementAt(i) );
    324      }
    325    }