001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    /*
004     * File: ModifiesGroupPragmaVec.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     * ModifiesGroupPragma should be globally replaced with the simple name of the
011     *              element type<p>
012     * escjava.ast should be globally replaced with the package the resulting
013     *              Vector type should live in<p>
014     * escjava.ast should be globally replaced with the package the
015     *              element type belongs to<p>
016     *
017     * The resulting type will have name ModifiesGroupPragmaVec.<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, ModifiesGroupPragmaVec'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     ** ModifiesGroupPragmaVec: A Vector of ModifiesGroupPragma'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 escjava.ast;
045    
046    
047    import java.util.Vector;
048    import javafe.util.StackVector;
049    
050    import escjava.ast.ModifiesGroupPragma;
051    
052    
053    public class  ModifiesGroupPragmaVec {
054    
055        /***************************************************
056         *                                                 *
057         * Instance fields:                                *
058         *                                                 *
059         ***************************************************/
060    
061        private /*@ spec_public non_null*/ ModifiesGroupPragma[] elements;
062        //@ invariant (\forall int i; (0<=i && i<count) ==> elements[i]!=null);
063        //@ invariant \typeof(elements) == \type(ModifiesGroupPragma[]);
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 ModifiesGroupPragmaVec(ModifiesGroupPragma[] els) {
083            this.count = els.length;
084            this.elements = new ModifiesGroupPragma[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 ModifiesGroupPragmaVec(int cnt) {
094            this.elements = new ModifiesGroupPragma[(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 ModifiesGroupPragmaVec make() { 
111            return new ModifiesGroupPragmaVec(0);
112        }
113    
114        //@ requires count >= 0;
115        //@ ensures \result!=null;
116        //@ ensures \fresh(\result);
117        public static ModifiesGroupPragmaVec make(int count) { 
118            return new ModifiesGroupPragmaVec(count);
119        }
120    
121        //@ requires vec!=null;
122        //@ requires vec.elementType <: \type(ModifiesGroupPragma);
123        //@ requires !vec.containsNull;
124        //@ ensures \result!=null;
125        //@ ensures \fresh(\result);
126        public static ModifiesGroupPragmaVec make(Vector vec) {
127            int sz = vec.size();
128            ModifiesGroupPragmaVec result = new ModifiesGroupPragmaVec(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 ModifiesGroupPragmaVec make(ModifiesGroupPragma[] els) {
140            return new ModifiesGroupPragmaVec(els);
141        }
142    
143        //
144        //@ requires s.vectorCount>1;
145        //@ requires s.elementType <: \type(ModifiesGroupPragma);
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 ModifiesGroupPragmaVec popFromStackVector(/*@non_null*/ StackVector s) {
153            // Creates a new ModifiesGroupPragmaVec from top stuff in StackVector
154            int sz = s.size();
155            ModifiesGroupPragmaVec r = new ModifiesGroupPragmaVec(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 ModifiesGroupPragma 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(ModifiesGroupPragma 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("{ModifiesGroupPragmaVec");
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 ModifiesGroupPragma[] toArray() {
213          int ct = count;
214          ModifiesGroupPragma[] b = new ModifiesGroupPragma[ 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 ModifiesGroupPragmaVec copy() {
224        ModifiesGroupPragmaVec result = new ModifiesGroupPragmaVec(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(ModifiesGroupPragma 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(ModifiesGroupPragma x) {
242        if( count == elements.length ) {
243          ModifiesGroupPragma[] newElements = new ModifiesGroupPragma[ 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(ModifiesGroupPragma 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 ModifiesGroupPragma pop() {
283            count--;
284            ModifiesGroupPragma 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(ModifiesGroupPragma obj, int index) {
302        if( count == elements.length ) {
303          ModifiesGroupPragma[] newElements = new ModifiesGroupPragma[ 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(ModifiesGroupPragmaVec 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    }