Package | Description |
---|---|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
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 | |
de.uka.ilkd.key.speclang.jml.translation |
Modifier and Type | Class and Description |
---|---|
class |
Do
Do.
|
class |
EnhancedFor
The new enhanced form of a for-loop.
|
class |
For
For.
|
class |
While
While.
|
Modifier and Type | Method and Description |
---|---|
void |
ProgVarReplaceVisitor.performActionOnLoopContract(LoopStatement oldLoop,
LoopStatement newLoop) |
void |
Visitor.performActionOnLoopContract(LoopStatement oldLoop,
LoopStatement newLoop)
Adds loop contract for new loop statement to loop contract
of old loop statement.
|
void |
JavaASTVisitor.performActionOnLoopContract(LoopStatement oldLoop,
LoopStatement newLoop) |
void |
ProgVarReplaceVisitor.performActionOnLoopInvariant(LoopStatement oldLoop,
LoopStatement newLoop) |
protected void |
CreatingASTVisitor.performActionOnLoopInvariant(LoopStatement oldLoop,
LoopStatement newLoop) |
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.copyLoopInvariant(LoopStatement from,
LoopStatement to)
Copies a loop invariant from a loop statement to another.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(LoopStatement loop)
Returns all loop contracts for the specified loop.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(LoopStatement loop,
Modality modality)
Returns loop contracts for according loop statement
and modality.
|
LoopSpecification |
SpecificationRepository.getLoopSpec(LoopStatement loop)
Returns the registered loop invariant for the passed loop, or null.
|
Modifier and Type | Method and Description |
---|---|
LoopStatement |
EnhancedForElimination.getLoop() |
Modifier and Type | Method and Description |
---|---|
void |
IntroAtPreDefsOp.updateBlockAndLoopContracts(ImmutableSet<StatementBlock> blocks,
ImmutableSet<LoopStatement> loops,
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 |
---|
ReattachLoopInvariant(LoopStatement ls) |
UnwindLoop(SchemaVariable innerLabel,
SchemaVariable outerLabel,
LoopStatement loop)
creates an unwind-loop ProgramTransformer
|
Modifier and Type | Method and Description |
---|---|
LoopStatement |
LoopContract.getLoop() |
LoopStatement |
LoopSpecification.getLoop()
Returns the loop to which the invariant belongs.
|
LoopStatement |
LoopContractImpl.getLoop() |
LoopStatement |
LoopSpecImpl.getLoop() |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
static AuxiliaryContract.Variables |
AuxiliaryContract.Variables.create(LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Creates a new instance.
|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
LoopStatement loop)
Returns the loop contracts for the passed loop.
|
LoopSpecification |
SpecExtractor.extractLoopInvariant(IProgramMethod pm,
LoopStatement loop)
Returns the loop invariant for the passed loop (if any).
|
LoopContract |
LoopContract.setLoop(LoopStatement newLoop) |
LoopSpecification |
LoopSpecification.setLoop(LoopStatement loop)
Returns a new loop invariant where the loop reference has been
replaced with the passed one.
|
LoopContract |
LoopContractImpl.setLoop(LoopStatement newLoop) |
LoopSpecification |
LoopSpecImpl.setLoop(LoopStatement loop) |
LoopContract |
LoopContract.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(LoopStatement newLoop,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy,
Term newDecreases) |
Constructor and Description |
---|
Creator(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
Services services)
Creates loop contract for a loop.
|
LoopContractImpl(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a loop.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres)
Creates an empty, default loop invariant for the passed loop.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
LoopStatement loop) |
LoopSpecification |
JMLSpecExtractor.extractLoopInvariant(IProgramMethod pm,
LoopStatement loop) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<LoopContract> |
JMLSpecFactory.createJMLLoopContracts(IProgramMethod method,
java.util.List<Label> labels,
LoopStatement loop,
TextualJMLSpecCase specificationCase)
Creates a set of loop contracts for a loop from a textual specification case.
|
LoopSpecification |
JMLSpecFactory.createJMLLoopInvariant(IProgramMethod pm,
LoopStatement loop,
TextualJMLLoopSpec textualLoopSpec) |
Copyright © 2003-2019 The KeY-Project.