| de.uka.ilkd.key.rule.metaconstruct.WhileLoopTransformation
 de.uka.ilkd.key.rule.metaconstruct.WhileInvariantTransformation
| WhileInvariantTransformation | | public class WhileInvariantTransformation extends WhileLoopTransformation (Code) | | Walks through a java AST in depth-left-fist-order.
This walker is used to transform a loop (not only
while loops) according to the rules of the dynamic logic.
|
| Constructor Summary | |
| public | WhileInvariantTransformation(ProgramElement root, ProgramElementName outerLabel, ProgramElementName innerLabel, ProgramVariable cont, ProgramVariable exc, ProgramVariable excParam, ProgramVariable thrownException, ProgramVariable brk, ProgramVariable rtrn, ProgramVariable returnExpr, LinkedList breakList, Services services)
| | public | WhileInvariantTransformation(ProgramElement root, SVInstantiations inst)
|
| WhileInvariantTransformation | | public WhileInvariantTransformation(ProgramElement root, ProgramElementName outerLabel, ProgramElementName innerLabel, ProgramVariable cont, ProgramVariable exc, ProgramVariable excParam, ProgramVariable thrownException, ProgramVariable brk, ProgramVariable rtrn, ProgramVariable returnExpr, LinkedList breakList, Services services)(Code) | | creates the WhileLoopTransformation for the transformation mode
Parameters:
root - the ProgramElement where to begin
Parameters:
outerLabel - the ProgramElementName of the outer label
Parameters:
innerLabel - the ProgramElementName of the inner label |
| WhileInvariantTransformation | | public WhileInvariantTransformation(ProgramElement root, SVInstantiations inst)(Code) | | creates the WhileLoopTransformation for the check mode
Parameters:
root - the ProgramElement where to begin
Parameters:
inst - the SVInstantiations if available |
| breakList | | public LinkedList breakList()(Code) | | returns a list of breaks that lead to
abrupt termination of the loop and
have to be replaced
|
| continueOccurred | | public boolean continueOccurred()(Code) | | returns true iff the loop to be transformed
contains a continue referring to this loop
|
| performActionOnAnnotationArray | | protected void performActionOnAnnotationArray(Annotation[] a)(Code) | | |
| performActionOnBreak | | public void performActionOnBreak(Break x)(Code) | | |
| performActionOnContinue | | public void performActionOnContinue(Continue x)(Code) | | |
| performActionOnReturn | | public void performActionOnReturn(Return x)(Code) | | |
| performActionOnWhile | | public void performActionOnWhile(While x)(Code) | | |
| returnOccurred | | public boolean returnOccurred()(Code) | | return true iff the loop to be transformed
contains a return statement leading to abrupt
termination of the loop body
|
|
|