Package | Description |
---|---|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.informationflow.po.snippet | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
Modifier and Type | Field and Description |
---|---|
ProofObligationVars |
IFProofObligationVars.c1 |
ProofObligationVars |
IFProofObligationVars.c2 |
ProofObligationVars |
IFProofObligationVars.symbExecVars |
Modifier and Type | Method and Description |
---|---|
java.util.Map<Term,Term> |
IFProofObligationVars.getMapFor(ProofObligationVars vars) |
Constructor and Description |
---|
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context) |
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
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.
|
IFProofObligationVars(ProofObligationVars c1,
ProofObligationVars c2,
ProofObligationVars symbExecVars) |
IFProofObligationVars(ProofObligationVars symbExecVars,
Services services) |
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.
|
SymbolicExecutionPO(InitConfig initConfig,
InformationFlowContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal) |
SymbolicExecutionPO(InitConfig initConfig,
InformationFlowContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
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(BlockContract contract,
ProofObligationVars vars,
ExecutionContext context,
Services services) |
static BasicPOSnippetFactory |
POSnippetFactory.getBasicFactory(FunctionalOperationContract contract,
ProofObligationVars vars,
Services services) |
static BasicPOSnippetFactory |
POSnippetFactory.getBasicFactory(InformationFlowContract contract,
ProofObligationVars vars,
Services services) |
static BasicPOSnippetFactory |
POSnippetFactory.getBasicFactory(LoopSpecification invariant,
ProofObligationVars vars,
ExecutionContext context,
Term guardTerm,
Services services) |
static InfFlowPOSnippetFactory |
POSnippetFactory.getInfFlowFactory(BlockContract contract,
ProofObligationVars vars1,
ProofObligationVars vars2,
ExecutionContext context,
Services services) |
static InfFlowPOSnippetFactory |
POSnippetFactory.getInfFlowFactory(InformationFlowContract contract,
ProofObligationVars vars1,
ProofObligationVars vars2,
Services services) |
static InfFlowPOSnippetFactory |
POSnippetFactory.getInfFlowFactory(LoopSpecification invariant,
ProofObligationVars vars1,
ProofObligationVars vars2,
ExecutionContext context,
Term guardTerm,
Services services) |
Term |
BasicLoopInvariantSnippet.produce(de.uka.ilkd.key.informationflow.po.snippet.BasicSnippetData d,
ProofObligationVars poVars) |
Term |
BasicFreeInvSnippet.produce(de.uka.ilkd.key.informationflow.po.snippet.BasicSnippetData d,
ProofObligationVars poVars) |
Term |
BasicLoopExecutionSnippet.produce(de.uka.ilkd.key.informationflow.po.snippet.BasicSnippetData d,
ProofObligationVars poVars) |
Term |
InfFlowLoopInvAppSnippet.produce(de.uka.ilkd.key.informationflow.po.snippet.BasicSnippetData d,
ProofObligationVars poVars1,
ProofObligationVars poVars2) |
Term |
SelfcomposedLoopSnippet.produce(de.uka.ilkd.key.informationflow.po.snippet.BasicSnippetData d,
ProofObligationVars poVars1,
ProofObligationVars poVars2) |
Modifier and Type | Method and Description |
---|---|
ProofObligationVars |
ProofObligationVars.labelHeapAtPreAsAnonHeapFunc() |
Constructor and Description |
---|
ProofObligationVars(ProofObligationVars orig,
java.lang.String postfix,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected static Term |
AbstractBlockContractRule.buildInfFlowPostAssumption(ProofObligationVars instVars,
ImmutableList<Term> localOuts,
ImmutableList<Term> localOutsAtPost,
Term baseHeap,
Term applPredTerm,
TermBuilder tb) |
protected static Term |
AbstractBlockContractRule.buildInfFlowPreAssumption(ProofObligationVars instVars,
ImmutableList<Term> localOuts,
ImmutableList<Term> localOutsAtPre,
Term baseHeap,
TermBuilder tb) |
Copyright © 2003-2019 The KeY-Project.