Package | Description |
---|---|
de.uka.ilkd.key.informationflow.proof | |
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
Constructor and Description |
---|
InfFlowProof(java.lang.String name,
Sequent sequent,
java.lang.String header,
TacletIndex rules,
BuiltInRuleIndex builtInRules,
InitConfig initConfig) |
Modifier and Type | Method and Description |
---|---|
abstract TacletIndex |
TacletIndex.copy()
copies the index
|
abstract TacletIndex |
TacletIndexKit.createTacletIndex()
abstract factory method to create an empty
TacletIndex |
abstract TacletIndex |
TacletIndexKit.createTacletIndex(java.lang.Iterable<Taclet> tacletSet)
abstract factory method to create a
TacletIndex containing the provided taclets |
TacletIndex |
Goal.indexOfTaclets()
returns the Taclet index for this goal.
|
TacletIndex |
RuleAppIndex.tacletIndex()
returns the Taclet index for this ruleAppIndex.
|
TacletIndex |
TacletAppIndex.tacletIndex()
returns the Taclet index for this ruleAppIndex.
|
Modifier and Type | Method and Description |
---|---|
TermTacletAppIndex |
TermTacletAppIndex.addTaclets(RuleFilter filter,
PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create a new tree of indices that additionally contain the taclets that
are selected by
filter |
SemisequentTacletAppIndex |
SemisequentTacletAppIndex.addTaclets(RuleFilter filter,
Sequent s,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create an index that additionally contains the taclets that are selected
by
filter |
static TermTacletAppIndex |
TermTacletAppIndex.create(PosInOccurrence pos,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener,
RuleFilter filter,
TermTacletAppIndexCacheSet indexCaches)
Create an index for the given term
|
void |
ProgVarReplacer.replace(TacletIndex tacletIndex)
replaces in the partially instantiated apps of a taclet index
|
SemisequentTacletAppIndex |
SemisequentTacletAppIndex.sequentChanged(SequentChangeInfo sci,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
called if a formula has been replaced
|
Constructor and Description |
---|
Proof(java.lang.String name,
Sequent sequent,
java.lang.String header,
TacletIndex rules,
BuiltInRuleIndex builtInRules,
InitConfig initConfig) |
RuleAppIndex(TacletIndex p_tacletIndex,
BuiltInRuleAppIndex p_builtInRuleAppIndex,
Services services) |
TacletAppIndex(TacletIndex tacletIndex,
Services services) |
Modifier and Type | Method and Description |
---|---|
TacletIndex |
InitConfig.createTacletIndex()
returns a newly created taclet index for the set of activated
taclets contained in this initial configuration
|
Copyright © 2003-2019 The KeY-Project.