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;
09:
10: import de.uka.ilkd.key.logic.*;
11: import de.uka.ilkd.key.java.statement.*;
12: import de.uka.ilkd.key.util.ExtList;
13: import de.uka.ilkd.key.rule.TacletForTests;
14:
15: /** this class is an example how to work with a java AST. Therefore we
16: * demonstrate the transformation of 'while (expr) { prg; }' to ' if
17: * (expr) then { prg; } while (expr) { prg }'
18: */
19:
20: public class RecoderExample {
21:
22: /** this method is used to create the part of the AST representing
23: * an if-then statement.
24: * @param expr the Expression that is the condition of the if part
25: * @param prg the JavaStatement after 'then'
26: * @return the If Statement with condition expr and 'then' part prg
27: */
28: public If createIfThen(Expression expr, JavaStatement prg) {
29: // create Then statement
30: Then _then = new Then(prg);
31: // create if part
32: return new If(expr, _then);
33: }
34:
35: /** transformates a "while(expr) {prg;}" to "if (exr) then {prg;}"
36: * @param While the while-loop to transform
37: * @return the transformed AST
38: */
39: public ExtList transform(While _while) {
40: ExtList stmnt = new ExtList();
41: stmnt.add(createIfThen(((Guard) _while.getGuard())
42: .getExpression(), (JavaStatement) _while.getBody()));
43: stmnt.add(_while);
44: return stmnt;
45: }
46:
47: /** transforms all while statements in a statement block to the wanted
48: * "if-then-while" statement
49: * @param prg the Statementblock to be transformed
50: */
51: public StatementBlock transform(StatementBlock prg) {
52: ExtList newBody = new ExtList();
53:
54: ArrayOfStatement body = prg.getBody();
55: for (int i = 0; i < body.size(); i++) {
56: if (body.getStatement(i) instanceof While) {
57: newBody.addAll(transform((While) body.getStatement(i)));
58: } else {
59: newBody.add(body.getStatement(i));
60: }
61: }
62: return new StatementBlock(newBody);
63: }
64:
65: /** test */
66: public static void main(String[] args) {
67: System.out.println("Starting...");
68: RecoderExample ex = new RecoderExample();
69: Recoder2KeY c2k = new Recoder2KeY(TacletForTests.services(),
70: new NamespaceSet());
71: String prg = "{ int i=0; while (i<5) { i++;} }";
72: JavaBlock block = c2k.readBlock(prg, c2k.createEmptyContext());
73: System.out.println("Read Original:\n" + block);
74: System.out.println("Transforming...");
75: System.out.println("Transformed:\n"
76: + (JavaBlock.createJavaBlock(ex
77: .transform((StatementBlock) block.program()))));
78: System.out.println("The original is left untouched:\n" + block);
79: }
80:
81: }
|