Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl |
Modifier and Type | Method and Description |
---|---|
While |
Recoder2KeYConverter.convert(While w)
converts a While.
|
static While |
KeYJavaASTFactory.whileLoop(Expression condition,
Statement body,
PositionInfo position)
Create a while loop at a specific source position.
|
Modifier and Type | Method and Description |
---|---|
void |
PrettyPrinter.printWhile(While x) |
void |
PrettyPrinter.printWhile(While x,
boolean includeBody) |
Modifier and Type | Method and Description |
---|---|
void |
Visitor.performActionOnWhile(While x) |
void |
OuterBreakContinueAndReturnReplacer.performActionOnWhile(While x) |
void |
InnerBreakAndContinueReplacer.performActionOnWhile(While x) |
void |
CreatingASTVisitor.performActionOnWhile(While x) |
void |
JavaASTVisitor.performActionOnWhile(While x) |
Modifier and Type | Field and Description |
---|---|
While |
AbstractLoopInvariantRule.Instantiation.loop |
Modifier and Type | Method and Description |
---|---|
While |
LoopInvariantBuiltInRuleApp.getLoopStatement() |
Constructor and Description |
---|
Instantiation(Term u,
Term progPost,
While loop,
LoopSpecification inv,
Term selfTerm,
ExecutionContext innermostExecutionContext) |
Modifier and Type | Method and Description |
---|---|
void |
WhileLoopTransformation.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. |
void |
ReplaceWhileLoop.performActionOnWhile(While x) |
void |
WhileInvariantTransformation.performActionOnWhile(While x) |
Modifier and Type | Method and Description |
---|---|
While |
ExecutionNodeReader.KeYlessLoopInvariant.getLoopStatement()
Returns the loop statement which is simulated by its loop invariant.
|
Modifier and Type | Method and Description |
---|---|
While |
IExecutionLoopInvariant.getLoopStatement()
Returns the loop statement which is simulated by its loop invariant.
|
Modifier and Type | Method and Description |
---|---|
While |
ExecutionLoopInvariant.getLoopStatement()
Returns the loop statement which is simulated by its loop invariant.
|
Copyright © 2003-2019 The KeY-Project.