Package | Description |
---|---|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
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.
|
Modifier and Type | Method and Description |
---|---|
RuleJustification |
Profile.getJustification(Rule r)
returns the (default) justification for the given rule
|
RuleJustification |
JavaProfile.getJustification(Rule r)
determines the justification of rule
r . |
RuleJustification |
AbstractProfile.getJustification(Rule r)
any standard rule has is by default justified by an axiom rule
justification
|
Modifier and Type | Method and Description |
---|---|
void |
InitConfig.registerRule(Rule r,
RuleJustification j)
registers a rule with the given justification at the
justification managing
RuleJustification object of this
environment. |
void |
InitConfig.registerRules(java.lang.Iterable<? extends Rule> s,
RuleJustification j)
registers a list of rules with the given justification at the
justification managing
RuleJustification object of this
environment. |
Modifier and Type | Interface and Description |
---|---|
interface |
ComplexRuleJustification |
Modifier and Type | Class and Description |
---|---|
class |
AxiomJustification |
class |
ComplexRuleJustificationBySpec |
class |
LemmaJustification
RuleJustification for taclets, that can be proven from other taclets. |
class |
RuleJustificationByAddRules |
class |
RuleJustificationBySpec |
Modifier and Type | Method and Description |
---|---|
RuleJustification |
RuleJustificationInfo.getJustification(Rule r) |
RuleJustification |
ProofCorrectnessMgt.getJustification(RuleApp r) |
RuleJustification |
RuleJustificationInfo.getJustification(RuleApp r,
TermServices services) |
RuleJustification |
ComplexRuleJustification.getSpecificJustification(RuleApp app,
TermServices services) |
RuleJustification |
ComplexRuleJustificationBySpec.getSpecificJustification(RuleApp app,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
void |
RuleJustificationInfo.addJustification(Rule r,
RuleJustification j) |
Modifier and Type | Method and Description |
---|---|
RuleJustification |
Taclet.getRuleJustification() |
Copyright © 2003-2019 The KeY-Project.