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.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml |
Modifier and Type | Method and Description |
---|---|
LabeledStatement |
Recoder2KeYConverter.convert(LabeledStatement l)
convert a labeled statement.
|
static LabeledStatement |
KeYJavaASTFactory.labeledStatement(ExtList parameters,
Label label,
PositionInfo position)
Create a labeled statement.
|
static LabeledStatement |
KeYJavaASTFactory.labeledStatement(Label label,
Statement statement,
PositionInfo pos)
Create a labeled statement.
|
Modifier and Type | Method and Description |
---|---|
void |
PrettyPrinter.printLabeledStatement(LabeledStatement x) |
Modifier and Type | Method and Description |
---|---|
protected LabeledStatement |
ProgramContextAdder.createLabeledStatementWrapper(LabeledStatement old,
JavaNonTerminalProgramElement body) |
Modifier and Type | Method and Description |
---|---|
protected LabeledStatement |
ProgramContextAdder.createLabeledStatementWrapper(LabeledStatement old,
JavaNonTerminalProgramElement body) |
void |
Visitor.performActionOnLabeledStatement(LabeledStatement x) |
void |
OuterBreakContinueAndReturnReplacer.performActionOnLabeledStatement(LabeledStatement x) |
void |
InnerBreakAndContinueReplacer.performActionOnLabeledStatement(LabeledStatement x) |
void |
CreatingASTVisitor.performActionOnLabeledStatement(LabeledStatement x) |
void |
JavaASTVisitor.performActionOnLabeledStatement(LabeledStatement x) |
Modifier and Type | Method and Description |
---|---|
void |
WhileLoopTransformation.performActionOnLabeledStatement(LabeledStatement x) |
Constructor and Description |
---|
DoBreak(LabeledStatement labeledBreak)
creates a do-break ProgramTransformer
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
SpecExtractor.extractBlockContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the block contracts for the passed labeled statement if it labels
a block.
|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the loop contracts for the passed labeled statement if it labels
a block.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
JMLSpecExtractor.extractBlockContracts(IProgramMethod method,
LabeledStatement labeled) |
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
LabeledStatement labeled) |
Copyright © 2003-2019 The KeY-Project.