Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.informationflow.po.snippet | |
de.uka.ilkd.key.informationflow.rule.tacletbuilder | |
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 |
This package contains classes for implementing rules.
|
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 | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
InvariantConfigurator.getLoopInvariant(LoopSpecification loopInv,
Services services,
boolean requiresVariant,
java.util.List<LocationVariable> heapContext)
Creates a Dialog.
|
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
InvariantConfigurator.getLoopInvariant(LoopSpecification loopInv,
Services services,
boolean requiresVariant,
java.util.List<LocationVariable> heapContext)
Creates a Dialog.
|
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
LoopInvExecutionPO.getLoopInvariant() |
Constructor and Description |
---|
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm) |
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
Modifier and Type | Method and Description |
---|---|
static BasicPOSnippetFactory |
POSnippetFactory.getBasicFactory(LoopSpecification invariant,
ProofObligationVars vars,
ExecutionContext context,
Term guardTerm,
Services services) |
static InfFlowPOSnippetFactory |
POSnippetFactory.getInfFlowFactory(LoopSpecification invariant,
ProofObligationVars vars1,
ProofObligationVars vars2,
ExecutionContext context,
Term guardTerm,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
InfFlowLoopInvariantTacletBuilder.setInvariant(LoopSpecification invariant) |
void |
LoopInfFlowUnfoldTacletBuilder.setLoopInv(LoopSpecification loopInv) |
Modifier and Type | Method and Description |
---|---|
void |
Visitor.performActionOnLoopInvariant(LoopSpecification x) |
void |
JavaASTVisitor.performActionOnLoopInvariant(LoopSpecification x) |
void |
ProgramVariableCollector.performActionOnLoopInvariant(LoopSpecification x) |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
SpecificationRepository.getLoopSpec(LoopStatement loop)
Returns the registered loop invariant for the passed loop, or null.
|
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addLoopInvariant(LoopSpecification inv)
Registers the passed loop invariant, possibly overwriting an older
registration for the same loop.
|
Modifier and Type | Field and Description |
---|---|
LoopSpecification |
AbstractLoopInvariantRule.Instantiation.inv |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
LoopInvariantBuiltInRuleApp.getSpec() |
LoopSpecification |
LoopInvariantBuiltInRuleApp.retrieveLoopInvariantFromSpecification(Services services) |
Modifier and Type | Method and Description |
---|---|
protected static AbstractLoopInvariantRule.AnonUpdateData |
AbstractLoopInvariantRule.createAnonUpdate(LocationVariable heap,
Term mod,
LoopSpecification inv,
Services services)
Computes the anonymizing update, the loop heap, the base heap, and the
anonymized heap.
|
LoopInvariantBuiltInRuleApp |
LoopInvariantBuiltInRuleApp.setLoopInvariant(LoopSpecification inv) |
Constructor and Description |
---|
Instantiation(Term u,
Term progPost,
While loop,
LoopSpecification inv,
Term selfTerm,
ExecutionContext innermostExecutionContext) |
LoopInvariantBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
LoopSpecification inv,
java.util.List<LocationVariable> heapContext,
TermServices services) |
LoopInvariantBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
LoopSpecification inv,
TermServices services) |
Modifier and Type | Class and Description |
---|---|
class |
LoopSpecImpl
Standard implementation of the LoopInvariant interface.
|
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
LoopSpecification.configurate(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)
Configure the existing loop specification element with new elements,
i.e., loop invariant clauses, a loop variant, modifies clauses,
information flow specification elements, and a loop variant,
possibly together with (if any) "free" loop invariant clauses.
|
LoopSpecification |
LoopSpecImpl.configurate(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) |
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) |
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) |
LoopSpecification |
SpecExtractor.extractLoopInvariant(IProgramMethod pm,
LoopStatement loop)
Returns the loop invariant for the passed loop (if any).
|
LoopSpecification |
LoopWellDefinedness.getStatement() |
LoopSpecification |
LoopSpecification.instantiate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term variant)
Instantiate a (raw) loop specification with loop invariant clauses and
a loop variant, possibly together with (if any) "free" loop invariant
clauses.
|
LoopSpecification |
LoopSpecImpl.instantiate(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term variant) |
LoopSpecification |
LoopSpecification.map(java.util.function.UnaryOperator<Term> op,
Services services) |
LoopSpecification |
LoopSpecImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
LoopSpecification |
LoopSpecification.setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns a new loop invariant where the invariant formula has been
replaced with the passed one.
|
LoopSpecification |
LoopSpecImpl.setInvariant(java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
LoopSpecification |
LoopSpecification.setLoop(LoopStatement loop)
Returns a new loop invariant where the loop reference has been
replaced with the passed one.
|
LoopSpecification |
LoopSpecImpl.setLoop(LoopStatement loop) |
LoopSpecification |
LoopSpecification.setTarget(IProgramMethod newPM) |
LoopSpecification |
LoopSpecImpl.setTarget(IProgramMethod newPM) |
LoopSpecification |
LoopSpecification.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
LoopSpecification |
LoopSpecImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Constructor and Description |
---|
LoopWellDefinedness(LoopSpecification inv,
ImmutableSet<ProgramVariable> params,
Services services) |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
JMLSpecExtractor.extractLoopInvariant(IProgramMethod pm,
LoopStatement loop) |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
JMLSpecFactory.createJMLLoopInvariant(IProgramMethod pm,
LoopStatement loop,
TextualJMLLoopSpec textualLoopSpec) |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
ExecutionNodeReader.KeYlessLoopInvariant.getLoopInvariant()
Returns the used
LoopSpecification . |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
IExecutionLoopInvariant.getLoopInvariant()
Returns the used
LoopSpecification . |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
ExecutionLoopInvariant.getLoopInvariant()
Returns the used
LoopSpecification . |
Modifier and Type | Method and Description |
---|---|
static java.util.Optional<LoopSpecification> |
MiscTools.getSpecForTermWithLoopStmt(Term loopTerm,
Services services)
Returns the
LoopSpecification for the program in the given term,
the active statement of which has to be a loop statement. |
Copyright © 2003-2019 The KeY-Project.