de.uka.ilkd.key.rule.metaconstruct

Class WhileInvariantTransformation

java.lang.Object

de.uka.ilkd.key.java.visitor.JavaASTWalker

de.uka.ilkd.key.java.visitor.JavaASTVisitor

de.uka.ilkd.key.rule.metaconstruct.WhileLoopTransformation

de.uka.ilkd.key.rule.metaconstruct.WhileInvariantTransformation

All Implemented Interfaces:

Visitor

public class WhileInvariantTransformation
extends WhileLoopTransformation

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.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.LinkedList<BreakToBeReplaced>	breakList
private ProgramVariable	brk
private ProgramVariable	cont
private boolean	continueOccurred
private ProgramVariable	exc
private ProgramVariable	excParam
private JavaInfo	javaInfo
private ProgramVariable	returnExpr
private boolean	returnOccurred
private ProgramVariable	rtrn
private ProgramVariable	thrownExc

Fields inherited from class de.uka.ilkd.key.rule.metaconstruct.WhileLoopTransformation

breakInnerLabel, breakOuterLabel, CHANGED, CHECK, instantiations, labelList, labelStack, methodStack, needInnerLabel, needOuterLabel, newLabels, replaceBreakWithNoLabel, replacement, result, runMode, stack, TRANSFORMATION

Fields inherited from class de.uka.ilkd.key.java.visitor.JavaASTVisitor

services

Constructor Summary

Constructors

Constructor and Description
WhileInvariantTransformation(ProgramElement root, ProgramElementName outerLabel, ProgramElementName innerLabel, ProgramVariable cont, ProgramVariable exc, ProgramVariable excParam, ProgramVariable thrownException, ProgramVariable brk, ProgramVariable rtrn, ProgramVariable returnExpr, java.util.LinkedList<BreakToBeReplaced> breakList, Services services) creates the WhileLoopTransformation for the transformation mode
WhileInvariantTransformation(ProgramElement root, SVInstantiations inst, Services services) creates the WhileLoopTransformation for the check mode

Method Summary

Modifier and Type	Method and Description
java.util.LinkedList<BreakToBeReplaced>	breakList() returns a list of breaks that lead to abrupt termination of the loop and have to be replaced
boolean	continueOccurred() returns true iff the loop to be transformed contains a continue referring to this loop
void	performActionOnBreak(Break x)
void	performActionOnContinue(Continue x)
void	performActionOnEnhancedFor(EnhancedFor x) Transform the body of an enhanced for loop for usage with invariant-theorems.
void	performActionOnReturn(Return x)
void	performActionOnWhile(While x) Performs the unwinding of the loop Warning: The unwinding does not comply with the rule in the KeY book up to 100% The difference is revealed by the following example: Label1:while(c){b} According to the KeY book the transformation should be if(c) l':{l'':{p#} Label1:while(c){b}} This implementation creates however.
boolean	returnOccurred() return true iff the loop to be transformed contains a return statement leading to abrupt termination of the loop body

Methods inherited from class de.uka.ilkd.key.rule.metaconstruct.WhileLoopTransformation

addChild, changed, doAction, doDefaultAction, innerLabelNeeded, outerLabelNeeded, performActionOnCase, performActionOnCatch, performActionOnCopyAssignment, performActionOnDefault, performActionOnDo, performActionOnElse, performActionOnFinally, performActionOnFor, performActionOnIf, performActionOnLabeledStatement, performActionOnLocalVariableDeclaration, performActionOnMethodFrame, performActionOnSchemaVariable, performActionOnStatementBlock, performActionOnSwitch, performActionOnSynchronizedBlock, performActionOnThen, performActionOnTry, replaceJumpStatement, result, start, toString, walk

Methods inherited from class de.uka.ilkd.key.java.visitor.JavaASTVisitor

performActionOnAbstractProgramElement, performActionOnAllFields, performActionOnAllObjects, performActionOnArrayDeclaration, performActionOnArrayInitializer, performActionOnArrayLengthReference, performActionOnArrayReference, performActionOnAssert, performActionOnBinaryAnd, performActionOnBinaryAndAssignment, performActionOnBinaryNot, performActionOnBinaryOr, performActionOnBinaryOrAssignment, performActionOnBinaryXOr, performActionOnBinaryXOrAssignment, performActionOnBlockContract, performActionOnBlockContract, performActionOnBooleanLiteral, performActionOnCatchAllStatement, performActionOnCharLiteral, performActionOnClassDeclaration, performActionOnClassInitializer, performActionOnComment, performActionOnCompilationUnit, performActionOnConditional, performActionOnConstructorDeclaration, performActionOnContextStatementBlock, performActionOnDivide, performActionOnDivideAssignment, performActionOnDLEmbeddedExpression, performActionOnDoubleLiteral, performActionOnEmptyMapLiteral, performActionOnEmptySeqLiteral, performActionOnEmptySetLiteral, performActionOnEmptyStatement, performActionOnEquals, performActionOnExactInstanceof, performActionOnExecutionContext, performActionOnExtends, performActionOnFieldDeclaration, performActionOnFieldReference, performActionOnFieldSpecification, performActionOnFloatLiteral, performActionOnForUpdates, performActionOnGreaterOrEquals, performActionOnGreaterThan, performActionOnGuard, performActionOnImplements, performActionOnImplicitFieldSpecification, performActionOnImport, performActionOnInstanceof, performActionOnInterfaceDeclaration, performActionOnIntersect, performActionOnIntLiteral, performActionOnIProgramVariable, performActionOnLessOrEquals, performActionOnLessThan, performActionOnLocationVariable, performActionOnLogicalAnd, performActionOnLogicalNot, performActionOnLogicalOr, performActionOnLongLiteral, performActionOnLoopContract, performActionOnLoopContract, performActionOnLoopContract, performActionOnLoopInit, performActionOnLoopInvariant, performActionOnLoopScopeBlock, performActionOnMergeContract, performActionOnMergePointStatement, performActionOnMetaClassReference, performActionOnMethod, performActionOnMethodBodyStatement, performActionOnMethodDeclaration, performActionOnMethodReference, performActionOnMinus, performActionOnMinusAssignment, performActionOnModifier, performActionOnModulo, performActionOnModuloAssignment, performActionOnNegative, performActionOnNew, performActionOnNewArray, performActionOnNotEquals, performActionOnNullLiteral, performActionOnPackageReference, performActionOnPackageSpecification, performActionOnParameterDeclaration, performActionOnParenthesizedExpression, performActionOnPassiveExpression, performActionOnPlus, performActionOnPlusAssignment, performActionOnPositive, performActionOnPostDecrement, performActionOnPostIncrement, performActionOnPreDecrement, performActionOnPreIncrement, performActionOnProgramConstant, performActionOnProgramElementName, performActionOnProgramMetaConstruct, performActionOnProgramMethod, performActionOnProgramVariable, performActionOnSchematicFieldReference, performActionOnSeqConcat, performActionOnSeqGet, performActionOnSeqIndexOf, performActionOnSeqLength, performActionOnSeqReverse, performActionOnSeqSingleton, performActionOnSeqSub, performActionOnSetMinus, performActionOnSetUnion, performActionOnShiftLeft, performActionOnShiftLeftAssignment, performActionOnShiftRight, performActionOnShiftRightAssignment, performActionOnSingleton, performActionOnStringLiteral, performActionOnSuperArrayDeclaration, performActionOnSuperConstructorReference, performActionOnSuperReference, performActionOnThisConstructorReference, performActionOnThisReference, performActionOnThrow, performActionOnThrows, performActionOnTimes, performActionOnTimesAssignment, performActionOnTransactionStatement, performActionOnTypeCast, performActionOnTypeReference, performActionOnUnsignedShiftRight, performActionOnUnsignedShiftRightAssignment, performActionOnVariableDeclaration, performActionOnVariableReference, performActionOnVariableSpecification

Methods inherited from class de.uka.ilkd.key.java.visitor.JavaASTWalker

depth, root

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

javaInfo

private JavaInfo javaInfo

cont

private ProgramVariable cont

exc

private ProgramVariable exc

rtrn

private ProgramVariable rtrn

brk

private ProgramVariable brk

thrownExc

private ProgramVariable thrownExc

excParam

private ProgramVariable excParam

returnExpr

private ProgramVariable returnExpr

continueOccurred

private boolean continueOccurred

returnOccurred

private boolean returnOccurred

breakList

private java.util.LinkedList<BreakToBeReplaced> breakList

Constructor Detail

WhileInvariantTransformation

public WhileInvariantTransformation(ProgramElement root,
                                    ProgramElementName outerLabel,
                                    ProgramElementName innerLabel,
                                    ProgramVariable cont,
                                    ProgramVariable exc,
                                    ProgramVariable excParam,
                                    ProgramVariable thrownException,
                                    ProgramVariable brk,
                                    ProgramVariable rtrn,
                                    ProgramVariable returnExpr,
                                    java.util.LinkedList<BreakToBeReplaced> breakList,
                                    Services services)

creates the WhileLoopTransformation for the transformation mode

Parameters:

root - the ProgramElement where to begin

outerLabel - the ProgramElementName of the outer label

innerLabel - the ProgramElementName of the inner label

WhileInvariantTransformation

public WhileInvariantTransformation(ProgramElement root,
                                    SVInstantiations inst,
                                    Services services)

creates the WhileLoopTransformation for the check mode

Parameters:

root - the ProgramElement where to begin

inst - the SVInstantiations if available

Method Detail

continueOccurred

public boolean continueOccurred()

returns true iff the loop to be transformed contains a continue referring to this loop

returnOccurred

public boolean returnOccurred()

return true iff the loop to be transformed contains a return statement leading to abrupt termination of the loop body

breakList

public java.util.LinkedList<BreakToBeReplaced> breakList()

returns a list of breaks that lead to abrupt termination of the loop and have to be replaced

performActionOnReturn

public void performActionOnReturn(Return x)

Specified by:

performActionOnReturn in interface Visitor

Overrides:

performActionOnReturn in class JavaASTVisitor

performActionOnContinue

public void performActionOnContinue(Continue x)

Specified by:

performActionOnContinue in interface Visitor

Overrides:

performActionOnContinue in class WhileLoopTransformation

performActionOnBreak

public void performActionOnBreak(Break x)

Specified by:

performActionOnBreak in interface Visitor

Overrides:

performActionOnBreak in class WhileLoopTransformation

performActionOnWhile

public void performActionOnWhile(While x)

Description copied from class: WhileLoopTransformation

Performs the unwinding of the loop Warning: The unwinding does not comply with the rule in the KeY book up to 100% The difference is revealed by the following example: Label1:while(c){b} According to the KeY book the transformation should be if(c) l':{l'':{p#} Label1:while(c){b}} This implementation creates however. Label1:if(c) l':{l'':{p#} while(c){b}} Check if this is ok when labeled continue statements are involved.

Specified by:

performActionOnWhile in interface Visitor

Overrides:

performActionOnWhile in class WhileLoopTransformation

Parameters:

x - the while statement

performActionOnEnhancedFor

public void performActionOnEnhancedFor(EnhancedFor x)

Transform the body of an enhanced for loop for usage with invariant-theorems. The following restriction is made for enhanced for loops: There is only one label (no inner/outer pair) needed, so innerlabel and outerlabel must be the same. The loop body is transformed like for a while loop (break/continue/return replaced, try+catch added). If the top loop is an enhancedFor-loop transform it like a while loop. Due to the fact that the condition in enhanced loops has no side effects, things can be put easier here. If the loop is not top most, act like the super class.

Specified by:

performActionOnEnhancedFor in interface Visitor

Overrides:

performActionOnEnhancedFor in class WhileLoopTransformation

Parameters:

x - EnhancedFor loop statement