001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010: //
011: //
012:
013: package de.uka.ilkd.key.java.statement;
014:
015: import de.uka.ilkd.key.java.*;
016: import de.uka.ilkd.key.java.annotation.Annotation;
017: import de.uka.ilkd.key.java.annotation.LoopInvariantAnnotation;
018: import de.uka.ilkd.key.util.ExtList;
019:
020: /**
021: * Loop statement.
022: *
023: */
024:
025: public abstract class LoopStatement extends JavaStatement implements
026: StatementContainer, ExpressionContainer {
027:
028: /**
029: * Inits.
030: */
031: protected final ILoopInit inits;
032:
033: /**
034: * Updates.
035: */
036: protected final IForUpdates updates;
037:
038: /**
039: * Guard.
040: */
041: protected final IGuard guard;
042:
043: /**
044: * Body.
045: */
046: protected final Statement body;
047:
048: protected Annotation[] annotations = new Annotation[0];
049:
050: /**
051: * Loop statement.
052: */
053: public LoopStatement() {
054: this .body = null;
055: this .updates = null;
056: this .inits = null;
057: this .guard = null;
058: }
059:
060: /**
061: * Loop statement.
062: * @param body a statement.
063: */
064: public LoopStatement(Statement body) {
065: this .body = body;
066: this .updates = null;
067: this .inits = null;
068: this .guard = null;
069: }
070:
071: /**
072: * Loop statement.
073: * @param guard the guard expression.
074: */
075: public LoopStatement(Expression guard) {
076: this .body = null;
077: this .updates = null;
078: this .inits = null;
079: this .guard = new Guard(guard);
080: }
081:
082: /**
083: * Loop statement.
084: * @param body a statement.
085: */
086: public LoopStatement(Expression guard, Statement body,
087: ExtList comments) {
088: super (comments);
089: this .body = body;
090: this .updates = null;
091: this .inits = null;
092: this .guard = new Guard(guard);
093: }
094:
095: public LoopStatement(Expression guard, Statement body,
096: ExtList comments, PositionInfo pos) {
097: super (add(comments, pos));
098: this .body = body;
099: this .updates = null;
100: this .inits = null;
101: this .guard = new Guard(guard);
102: }
103:
104: /**
105: * Loop statement.
106: * @param body a statement.
107: */
108: public LoopStatement(Expression guard, Statement body,
109: Annotation[] a) {
110: this .body = body;
111: this .updates = null;
112: this .inits = null;
113: this .guard = new Guard(guard);
114: this .annotations = a;
115: }
116:
117: public LoopStatement(Expression guard, Statement body,
118: Annotation[] a, PositionInfo pos) {
119: super (add(new ExtList(), pos));
120: this .body = body;
121: this .updates = null;
122: this .inits = null;
123: this .guard = new Guard(guard);
124: this .annotations = a;
125: }
126:
127: /**
128: * Loop statement. This constructor is used for the transformation
129: * of Recoder to KeY.
130: * @param inits the initializers of the loop
131: * @param guard the guard of the loop
132: * @param updates the updates of the loop
133: * @param body the body of the loop
134: */
135: public LoopStatement(LoopInitializer[] inits, Expression guard,
136: Expression[] updates, Statement body) {
137: this .body = body;
138: if (updates != null) {
139: this .updates = new ForUpdates(
140: new ArrayOfExpression(updates));
141: } else {
142: this .updates = new ForUpdates(new ArrayOfExpression(
143: new Expression[0]));
144: }
145: this .inits = new LoopInit(inits);
146: this .guard = new Guard(guard);
147: }
148:
149: /**
150: * Loop statement. This constructor is used for the transformation
151: * of Recoder to KeY.
152: * @param inits the initializers of the loop
153: * @param guard the guard of the loop
154: * @param updates the updates of the loop
155: * @param body the body of the loop
156: * @param comments the comments attached to this statement.
157: */
158: public LoopStatement(ILoopInit inits, IGuard guard,
159: IForUpdates updates, Statement body, ExtList comments) {
160: super (comments);
161: this .body = body;
162: this .updates = updates;
163: this .inits = inits;
164: this .guard = guard;
165: this .annotations = (Annotation[]) comments
166: .collect(Annotation.class);
167: }
168:
169: public LoopStatement(ILoopInit inits, IGuard guard,
170: IForUpdates updates, Statement body, ExtList comments,
171: PositionInfo pos) {
172: super (add(comments, pos));
173: this .body = body;
174: this .updates = updates;
175: this .inits = inits;
176: this .guard = guard;
177: this .annotations = (Annotation[]) comments
178: .collect(Annotation.class);
179: }
180:
181: /**
182: * Loop statement. This constructor is used for the transformation
183: * of Recoder to KeY.
184: * @param inits the initializers of the loop
185: * @param guard the guard of the loop
186: * @param updates the updates of the loop
187: * @param body the body of the loop
188: */
189: public LoopStatement(ILoopInit inits, IGuard guard,
190: IForUpdates updates, Statement body) {
191: this .body = body;
192: this .updates = updates;
193: this .inits = inits;
194: this .guard = guard;
195: }
196:
197: static private ExtList add(ExtList e, Object o) {
198: e.add(o);
199: return e;
200: }
201:
202: /**
203: * Returns the number of children of this node.
204: * @return an int giving the number of children of this node
205: */
206: public int getChildCount() {
207: int result = 0;
208: if (inits != null)
209: result++;
210: if (guard != null)
211: result++;
212: if (updates != null)
213: result++;
214: if (body != null)
215: result++;
216: return result;
217: }
218:
219: /**
220: * Returns the child at the specified index in this node's "virtual"
221: * child array
222: * @param index an index into this node's "virtual" child array
223: * @return the program element at the given position
224: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
225: * of bounds
226: */
227: public ProgramElement getChildAt(int index) {
228: if (inits != null) {
229: if (index == 0) {
230: return inits;
231: }
232: index--;
233: }
234: if (isCheckedBeforeIteration()) {
235: if (guard != null) {
236: if (index == 0)
237: return guard;
238: index--;
239: }
240: }
241: if (updates != null) {
242: if (index == 0) {
243: return updates;
244: }
245: index--;
246: }
247: if (body != null) {
248: if (index == 0)
249: return body;
250: index--;
251: }
252: if (!isCheckedBeforeIteration()) {
253: if (guard != null) {
254: if (index == 0)
255: return guard;
256: index--;
257: }
258: }
259: throw new ArrayIndexOutOfBoundsException();
260: }
261:
262: /**
263: * Get the number of expressions in this container.
264: * @return the number of expressions.
265: */
266: public int getExpressionCount() {
267: int result = 0;
268: if (guard != null)
269: result += 1;
270: if (inits != null) {
271: result += 1;
272: }
273: if (updates != null) {
274: result += updates.size();
275: }
276: return result;
277: }
278:
279: /*
280: Return the expression at the specified index in this node's
281: "virtual" expression array.
282: @param index an index for an expression.
283: @return the expression with the given index.
284: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
285: of bounds.
286: */
287: public Expression getExpressionAt(int index) {
288: if (guard != null) {
289: if (index == 0) {
290: return (Expression) guard.getChildAt(0);
291: }
292: index -= 1;
293: }
294: if (inits != null) {
295: int s = inits.size();
296: for (int i = 0; i < s && index >= 0; i++) {
297: final LoopInitializer ii = inits.getInits()
298: .getLoopInitializer(i);
299: if (ii instanceof Expression) {
300: if (index == 0) {
301: return (Expression) ii;
302: }
303: index -= 1;
304: }
305: }
306: }
307: if (updates != null) {
308: return updates.getExpressionAt(index);
309: }
310: throw new ArrayIndexOutOfBoundsException();
311: }
312:
313: /**
314: * Get guard.
315: * @return the expression.
316: */
317: public IGuard getGuard() {
318: return guard;
319: }
320:
321: /**
322: * Get guard.
323: * @return the expression.
324: */
325: public Expression getGuardExpression() {
326: return (Expression) guard.getChildAt(0);
327: }
328:
329: /**
330: * Get body.
331: * @return the statement.
332: */
333: public Statement getBody() {
334: return body;
335: }
336:
337: /**
338: * Get the number of statements in this container.
339: * @return the number of statements.
340: */
341: public int getStatementCount() {
342: return (body != null) ? 1 : 0;
343: }
344:
345: /*
346: Return the statement at the specified index in this node's
347: "virtual" statement array.
348: @param index an index for a statement.
349: @return the statement with the given index.
350: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
351: of bounds.
352: */
353: public Statement getStatementAt(int index) {
354: if (body != null && index == 0) {
355: return body;
356: }
357: throw new ArrayIndexOutOfBoundsException();
358: }
359:
360: /**
361: * Get initializers.
362: * @return the loop initializer array wrapper .
363: */
364: public ArrayOfLoopInitializer getInitializers() {
365: if (inits != null) {
366: return inits.getInits();
367: }
368: return null;
369: }
370:
371: /**
372: * Get updates.
373: * @return the expression mutable list.
374: */
375: public ArrayOfExpression getUpdates() {
376: if (updates != null) {
377: return updates.getUpdates();
378: }
379: return null;
380: }
381:
382: /**
383: * Get updates as IForUpdates
384: * @return the expression mutable list.
385: */
386: public IForUpdates getIForUpdates() {
387: return updates;
388: }
389:
390: /**
391: *@return the annotations.
392: */
393: public Annotation[] getAnnotations() {
394: return annotations;
395: }
396:
397: public int getAnnotationCount() {
398: return annotations.length;
399: }
400:
401: /**
402: * Don't use this method !!!
403: */
404: // HACK: loop invariants are parsed after this LoopStatement has already
405: // been created, that's why they are set afterwards.
406: // TODO: find a better solution which is compatible with the immutability
407: // of ProgramElements.
408: public void addLoopInvariant(LoopInvariantAnnotation a) {
409: Annotation[] result = new Annotation[annotations.length + 1];
410: for (int i = 0; i < annotations.length; i++) {
411: result[i] = annotations[i];
412: }
413: result[annotations.length] = a;
414: annotations = result;
415: }
416:
417: /**
418: * Is exit condition.
419: * @return the boolean value.
420: */
421: public abstract boolean isExitCondition();
422:
423: /**
424: * Is checked before iteration.
425: * @return the boolean value.
426: */
427: public abstract boolean isCheckedBeforeIteration();
428: }
|