001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 /* 004 * File: GuardedCmdVec.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 * GuardedCmd 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 GuardedCmdVec.<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, GuardedCmdVec'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 ** GuardedCmdVec: A Vector of GuardedCmd'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.GuardedCmd; 051 052 053 public class GuardedCmdVec { 054 055 /*************************************************** 056 * * 057 * Instance fields: * 058 * * 059 ***************************************************/ 060 061 private /*@ spec_public non_null*/ GuardedCmd[] elements; 062 //@ invariant (\forall int i; (0<=i && i<count) ==> elements[i]!=null); 063 //@ invariant \typeof(elements) == \type(GuardedCmd[]); 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 GuardedCmdVec(GuardedCmd[] els) { 083 this.count = els.length; 084 this.elements = new GuardedCmd[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 GuardedCmdVec(int cnt) { 094 this.elements = new GuardedCmd[(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 GuardedCmdVec make() { 111 return new GuardedCmdVec(0); 112 } 113 114 //@ requires count >= 0; 115 //@ ensures \result!=null; 116 //@ ensures \fresh(\result); 117 public static GuardedCmdVec make(int count) { 118 return new GuardedCmdVec(count); 119 } 120 121 //@ requires vec!=null; 122 //@ requires vec.elementType <: \type(GuardedCmd); 123 //@ requires !vec.containsNull; 124 //@ ensures \result!=null; 125 //@ ensures \fresh(\result); 126 public static GuardedCmdVec make(Vector vec) { 127 int sz = vec.size(); 128 GuardedCmdVec result = new GuardedCmdVec(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 GuardedCmdVec make(GuardedCmd[] els) { 140 return new GuardedCmdVec(els); 141 } 142 143 // 144 //@ requires s.vectorCount>1; 145 //@ requires s.elementType <: \type(GuardedCmd); 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 GuardedCmdVec popFromStackVector(/*@non_null*/ StackVector s) { 153 // Creates a new GuardedCmdVec from top stuff in StackVector 154 int sz = s.size(); 155 GuardedCmdVec r = new GuardedCmdVec(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 GuardedCmd 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(GuardedCmd 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("{GuardedCmdVec"); 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 GuardedCmd[] toArray() { 213 int ct = count; 214 GuardedCmd[] b = new GuardedCmd[ 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 GuardedCmdVec copy() { 224 GuardedCmdVec result = new GuardedCmdVec(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(GuardedCmd 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(GuardedCmd x) { 242 if( count == elements.length ) { 243 GuardedCmd[] newElements = new GuardedCmd[ 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(GuardedCmd 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 GuardedCmd pop() { 283 count--; 284 GuardedCmd 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(GuardedCmd obj, int index) { 302 if( count == elements.length ) { 303 GuardedCmd[] newElements = new GuardedCmd[ 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(GuardedCmdVec 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 }