Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
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.speclang |
This package contains the specification language frontends of KeY.
|
Modifier and Type | Class and Description |
---|---|
class |
ContextStatementBlock
In the DL-formulae description of Taclets the program part can have
the following form < pi alpha;...; omega > Phi where pi is a prefix
consisting of open brackets, try's and so on and omega is the rest
of the program.
|
class |
StatementBlock
Statement block.
|
Modifier and Type | Class and Description |
---|---|
class |
Assert |
class |
BranchStatement
Branch statement.
|
class |
Break
Break.
|
class |
Continue
Continue.
|
class |
Do
Do.
|
class |
EnhancedFor
The new enhanced form of a for-loop.
|
class |
Exec
Exec.
|
class |
ExpressionJumpStatement
Expression jump statement.
|
class |
For
For.
|
class |
If
If.
|
class |
JumpStatement
Jump statement.
|
class |
LabeledStatement
Labeled statement.
|
class |
LabelJumpStatement
Label jump statement.
|
class |
LoopScopeBlock
Loop scope block.
|
class |
LoopStatement
Loop statement.
|
class |
MergePointStatement
A statement indicating a merge point.
|
class |
MethodFrame
The statement inserted by KeY if a method call is executed.
|
class |
Return
Return.
|
class |
Switch
Switch.
|
class |
SynchronizedBlock
Synchronized block.
|
class |
Throw
Throw.
|
class |
TransactionStatement |
class |
Try
Try.
|
class |
While
While.
|
Modifier and Type | Field and Description |
---|---|
JavaStatement |
AbstractAuxiliaryContractRule.Instantiation.statement
The statement the contract belongs to.
|
Modifier and Type | Method and Description |
---|---|
JavaStatement |
AbstractAuxiliaryContractBuiltInRuleApp.getStatement() |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<BlockContract> |
AbstractBlockContractRule.getApplicableContracts(SpecificationRepository specifications,
JavaStatement statement,
Modality modality,
Goal goal) |
static ImmutableSet<LoopContract> |
AbstractLoopContractRule.getApplicableContracts(SpecificationRepository specifications,
JavaStatement statement,
Modality modality,
Goal goal) |
protected boolean |
AbstractBlockContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement statement,
Modality modality,
Goal goal) |
protected abstract boolean |
AbstractAuxiliaryContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement element,
Modality modality,
Goal goal) |
protected boolean |
AbstractLoopContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement statement,
Modality modality,
Goal goal) |
void |
AbstractAuxiliaryContractBuiltInRuleApp.setStatement(JavaStatement s) |
void |
AbstractBlockContractBuiltInRuleApp.update(JavaStatement statement,
BlockContract contract,
java.util.List<LocationVariable> heaps) |
void |
AbstractLoopContractBuiltInRuleApp.update(JavaStatement statement,
LoopContract contract,
java.util.List<LocationVariable> heaps) |
Modifier and Type | Method and Description |
---|---|
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<? extends JavaStatement> statements,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.Map<LocationVariable,LocationVariable> atPreHeapVars,
Services services)
Replace the placeholder variables
(see
AuxiliaryContract.getPlaceholderVariables() )
of all block contracts for blocks in blocks by
atPreVars and atPreHeapVars |
Constructor and Description |
---|
VariablesCreator(JavaStatement statement,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Constructor.
|
Copyright © 2003-2019 The KeY-Project.