public class WhileInvariantTransformation extends WhileLoopTransformation
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 |
breakInnerLabel, breakOuterLabel, CHANGED, CHECK, instantiations, labelList, labelStack, methodStack, needInnerLabel, needOuterLabel, newLabels, replaceBreakWithNoLabel, replacement, result, runMode, stack, TRANSFORMATION
services
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
|
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
|
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
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
depth, root
private JavaInfo javaInfo
private ProgramVariable cont
private ProgramVariable exc
private ProgramVariable rtrn
private ProgramVariable brk
private ProgramVariable thrownExc
private ProgramVariable excParam
private ProgramVariable returnExpr
private boolean continueOccurred
private boolean returnOccurred
private java.util.LinkedList<BreakToBeReplaced> breakList
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)
root
- the ProgramElement where to beginouterLabel
- the ProgramElementName of the outer labelinnerLabel
- the ProgramElementName of the inner labelpublic WhileInvariantTransformation(ProgramElement root, SVInstantiations inst, Services services)
root
- the ProgramElement where to begininst
- the SVInstantiations if availablepublic boolean continueOccurred()
public boolean returnOccurred()
public java.util.LinkedList<BreakToBeReplaced> breakList()
public void performActionOnReturn(Return x)
performActionOnReturn
in interface Visitor
performActionOnReturn
in class JavaASTVisitor
public void performActionOnContinue(Continue x)
performActionOnContinue
in interface Visitor
performActionOnContinue
in class WhileLoopTransformation
public void performActionOnBreak(Break x)
performActionOnBreak
in interface Visitor
performActionOnBreak
in class WhileLoopTransformation
public void performActionOnWhile(While x)
WhileLoopTransformation
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.performActionOnWhile
in interface Visitor
performActionOnWhile
in class WhileLoopTransformation
x
- the while statementpublic void performActionOnEnhancedFor(EnhancedFor x)
performActionOnEnhancedFor
in interface Visitor
performActionOnEnhancedFor
in class WhileLoopTransformation
x
- EnhancedFor loop statement