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: * Do.
20: *
21: */
22: public class Do extends LoopStatement {
23:
24: /**
25: * Do.
26: */
27: public Do() {
28: super ();
29: }
30:
31: /**
32: * Do.
33: * @param guard an expression.
34: */
35: public Do(Expression guard) {
36: super (guard);
37: }
38:
39: /**
40: * Do.
41: * @param guard an expression.
42: * @param body a statement.
43: */
44: public Do(Expression guard, Statement body, ExtList l,
45: PositionInfo pos) {
46: super (guard, body, l, pos);
47: }
48:
49: /**
50: * Do.
51: * @param guard an expression.
52: * @param body a statement.
53: */
54: public Do(Expression guard, Statement body, PositionInfo pos,
55: Annotation[] a) {
56: super (guard, body, a, pos);
57: }
58:
59: public SourceElement getLastElement() {
60: return this ;
61: }
62:
63: /**
64: * Is exit condition.
65: * @return the boolean value.
66: */
67: public boolean isExitCondition() {
68: return false;
69: }
70:
71: /**
72: * Is checked before iteration.
73: * @return the boolean value.
74: */
75: public boolean isCheckedBeforeIteration() {
76: return false;
77: }
78:
79: /** calls the corresponding method of a visitor in order to
80: * perform some action/transformation on this element
81: * @param v the Visitor
82: */
83: public void visit(Visitor v) {
84: v.performActionOnDo(this );
85: }
86:
87: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
88: p.printDo(this);
89: }
90: }
|