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.rule.metaconstruct;
12:
13: import de.uka.ilkd.key.java.ProgramElement;
14: import de.uka.ilkd.key.java.Services;
15: import de.uka.ilkd.key.java.statement.LoopStatement;
16: import de.uka.ilkd.key.logic.ProgramElementName;
17: import de.uka.ilkd.key.logic.op.SchemaVariable;
18: import de.uka.ilkd.key.rule.inst.SVInstantiations;
19:
20: /**
21: * This class is used to perform program transformations needed
22: * for the symbolic execution of a loop. It unwinds the loop:
23: * e.g.
24: * <code>
25: * while ( i<10 ) {
26: * i++
27: * }
28: * </code> becomes
29: * <code>
30: * l1: {
31: * if (i<10) { i++}
32: * else break l1;
33: * l2: {
34: * while ( i<10 ) {
35: * i++
36: * }
37: * }}
38: * </code> becomes
39: */
40: public class UnwindLoop extends ProgramMetaConstruct {
41:
42: /** the outer label that is used to leave the while loop ('l1') */
43: private final SchemaVariable outerLabel;
44: /** the inner label ('l2') */
45: private final SchemaVariable innerLabel;
46:
47: /** creates an unwind-loop ProgramMetaConstruct
48: * @param loop the LoopStatement contained by the meta construct
49: */
50: public UnwindLoop(SchemaVariable innerLabel,
51: SchemaVariable outerLabel, LoopStatement loop) {
52: super ("#unwind-loop", loop);
53: this .innerLabel = innerLabel;
54: this .outerLabel = outerLabel;
55: }
56:
57: /** performs the program transformation needed for symbolic
58: * program transformation
59: * @param services the Services with all necessary information
60: * about the java programs
61: * @param svInst the instantiations esp. of the inner and outer label
62: * @return the transformated program
63: */
64: public ProgramElement symbolicExecution(ProgramElement pe,
65: Services services, SVInstantiations svInst) {
66: if (!(pe instanceof LoopStatement)) {
67: return pe;
68: }
69: final LoopStatement originalLoop = (LoopStatement) pe;
70:
71: final WhileLoopTransformation w = new WhileLoopTransformation(
72: originalLoop, (ProgramElementName) svInst
73: .getInstantiation(outerLabel),
74: (ProgramElementName) svInst
75: .getInstantiation(innerLabel));
76: w.start();
77: return w.result();
78: }
79:
80: public SchemaVariable getInnerLabelSV() {
81: return innerLabel;
82: }
83:
84: public SchemaVariable getOuterLabelSV() {
85: return outerLabel;
86: }
87: }
|