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