01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.java.statement;
12:
13: import de.uka.ilkd.key.java.*;
14: import de.uka.ilkd.key.java.annotation.Annotation;
15: import de.uka.ilkd.key.java.visitor.Visitor;
16: import de.uka.ilkd.key.util.ExtList;
17:
18: /**
19: * While.
20: */
21:
22: public class While extends LoopStatement {
23:
24: /**
25: * While.
26: */
27:
28: public While() {
29: }
30:
31: /**
32: * While.
33: * @param guard an expression.
34: * @param body a statement.
35: * @param pos a PositionInformation.
36: */
37:
38: public While(Expression guard, Statement body, PositionInfo pos,
39: ExtList comments) {
40: super (guard, body, comments, pos);
41: }
42:
43: /**
44: * While.
45: * @param guard an expression.
46: * @param body a statement.
47: * @param pos a PositionInformation.
48: */
49:
50: public While(Expression guard, Statement body, PositionInfo pos,
51: Annotation[] a) {
52: super (guard, body, a, pos);
53: }
54:
55: public SourceElement getLastElement() {
56: return (body != null) ? body.getLastElement() : this ;
57: }
58:
59: /**
60: * Is exit condition.
61: * @return the boolean value.
62: */
63:
64: public boolean isExitCondition() {
65: return false;
66: }
67:
68: /**
69: * Is checked before iteration.
70: * @return the boolean value.
71: */
72:
73: public boolean isCheckedBeforeIteration() {
74: return true;
75: }
76:
77: /** calls the corresponding method of a visitor in order to
78: * perform some action/transformation on this element
79: * @param v the Visitor
80: */
81: public void visit(Visitor v) {
82: v.performActionOnWhile(this );
83: }
84:
85: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
86: p.printWhile(this);
87: }
88: }
|