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: package de.uka.ilkd.key.java.statement;
012:
013: import de.uka.ilkd.key.java.PrettyPrinter;
014: import de.uka.ilkd.key.java.ProgramElement;
015: import de.uka.ilkd.key.java.SourceElement;
016: import de.uka.ilkd.key.java.Statement;
017: import de.uka.ilkd.key.java.visitor.Visitor;
018: import de.uka.ilkd.key.util.ExtList;
019:
020: /**
021: * Then.
022: * @author <TT>AutoDoc</TT>
023: */
024:
025: public class Then extends BranchImp {
026:
027: /**
028: * Body.
029: */
030:
031: protected Statement body;
032:
033: /**
034: * Constructor for the transformation of COMPOST ASTs to KeY.
035: * @param children the children of this AST element as KeY classes.
036: */
037: public Then(ExtList children) {
038: super (children);
039: body = (Statement) children.get(Statement.class);
040: }
041:
042: /**
043: * Constructor for the transformation of COMPOST ASTs to KeY.
044: * @param stmnt the statement part of Then.
045: */
046: public Then(Statement stmnt) {
047: this .body = stmnt;
048: }
049:
050: public SourceElement getFirstElement() {
051: return body.getFirstElement();
052: }
053:
054: public SourceElement getLastElement() {
055: return body.getLastElement();
056: }
057:
058: /**
059: * Returns the number of children of this node.
060: * @return an int giving the number of children of this node
061: */
062:
063: public int getChildCount() {
064: return (body != null) ? 1 : 0;
065: }
066:
067: /**
068: * Returns the child at the specified index in this node's "virtual"
069: * child array
070: * @param index an index into this node's "virtual" child array
071: * @return the program element at the given position
072: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
073: * of bounds
074: */
075:
076: public ProgramElement getChildAt(int index) {
077: if (body != null) {
078: if (index == 0)
079: return body;
080: }
081: throw new ArrayIndexOutOfBoundsException();
082: }
083:
084: /**
085: * Get the number of statements in this container.
086: * @return the number of statements.
087: */
088:
089: public int getStatementCount() {
090: return (body != null) ? 1 : 0;
091: }
092:
093: /*
094: Return the statement at the specified index in this node's
095: "virtual" statement array.
096: @param index an index for a statement.
097: @return the statement with the given index.
098: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
099: of bounds.
100: */
101:
102: public Statement getStatementAt(int index) {
103: if (body != null && index == 0) {
104: return body;
105: }
106: throw new ArrayIndexOutOfBoundsException();
107: }
108:
109: /**
110: * The body may be empty (null), to define a fall-through.
111: * Attaching an {@link EmptyStatement} would create a single ";".
112: */
113: public Statement getBody() {
114: return body;
115: }
116:
117: /** calls the corresponding method of a visitor in order to
118: * perform some action/transformation on this element
119: * @param v the Visitor
120: */
121: public void visit(Visitor v) {
122: v.performActionOnThen(this );
123: }
124:
125: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
126: p.printThen(this);
127: }
128: }
|