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: package de.uka.ilkd.key.java.statement;
09:
10: import de.uka.ilkd.key.java.*;
11: import de.uka.ilkd.key.java.visitor.Visitor;
12:
13: public class Assert extends JavaStatement implements
14: ExpressionContainer {
15:
16: private Expression condition;
17: private Expression message;
18:
19: public Assert(Expression condition, Expression message,
20: PositionInfo pos) {
21: super (pos);
22: assert condition != null;
23: this .condition = condition;
24: this .message = message;
25: }
26:
27: public Expression getExpressionAt(int index) {
28: if (index == 0) {
29: return condition;
30: }
31: index--;
32: if (index == 0) {
33: if (message != null) {
34: return message;
35: }
36: }
37: throw new IndexOutOfBoundsException();
38: }
39:
40: public int getExpressionCount() {
41: return message == null ? 1 : 2;
42: }
43:
44: public ProgramElement getChildAt(int index) {
45: return getExpressionAt(index);
46: }
47:
48: public int getChildCount() {
49: return getExpressionCount();
50: }
51:
52: public void visit(Visitor v) {
53: v.performActionOnAssert(this );
54: }
55:
56: public Expression getCondition() {
57: return condition;
58: }
59:
60: public Expression getMessage() {
61: return message;
62: }
63:
64: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
65: p.printAssert(this);
66: }
67: }
|