Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
de.uka.ilkd.key.control.instantiation_model | |
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.executor.javadl | |
de.uka.ilkd.key.rule.match.legacy | |
de.uka.ilkd.key.rule.match.vm | |
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
Constructor and Description |
---|
SearchNode(SequentFormula[] pattern,
int succAntPos,
ImmutableList<IfFormulaInstantiation> antec,
ImmutableList<IfFormulaInstantiation> succ) |
SearchNode(SequentFormula[] pattern,
int succAntPos,
ImmutableList<IfFormulaInstantiation> antec,
ImmutableList<IfFormulaInstantiation> succ) |
Modifier and Type | Method and Description |
---|---|
static IfFormulaInstantiation[] |
TacletAssumesModel.createIfInsts(ImmutableList<IfFormulaInstantiation> candidates) |
IfFormulaInstantiation |
TacletAssumesModel.getSelection(int pos) |
Modifier and Type | Method and Description |
---|---|
static IfFormulaInstantiation[] |
TacletAssumesModel.createIfInsts(ImmutableList<IfFormulaInstantiation> candidates) |
Constructor and Description |
---|
TacletAssumesModel(Term ifFma,
ImmutableList<IfFormulaInstantiation> candidates,
TacletApp app,
Goal goal,
Services services,
NamespaceSet nss,
AbbrevMap scm) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
OutputStreamProofSaver.ifFormulaInsts(Node node,
ImmutableList<IfFormulaInstantiation> l) |
Modifier and Type | Class and Description |
---|---|
class |
IfFormulaInstDirect
Instantiation of an if-formula that has to be proven by an explicit
if-goal
|
class |
IfFormulaInstSeq
Instantiation of an if-formula that is a formula of an existing
sequent.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<IfFormulaInstantiation> |
TacletApp.ifInstantiations
chosen instantiations for the if sequent formulas
|
Modifier and Type | Method and Description |
---|---|
static ImmutableList<IfFormulaInstantiation> |
IfFormulaInstSeq.createList(Sequent p_s,
boolean antec,
Services services) |
ImmutableList<IfFormulaInstantiation> |
IfFormulaInstantiationCache.get(boolean antec,
Semisequent s) |
ImmutableList<IfFormulaInstantiation> |
IfMatchResult.getFormulas() |
ImmutableList<IfFormulaInstantiation> |
TacletApp.ifFormulaInstantiations() |
Modifier and Type | Method and Description |
---|---|
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
PosInOccurrence pos,
Services services) |
protected static boolean |
TacletApp.ifInstsCorrectSize(Taclet p_taclet,
ImmutableList<IfFormulaInstantiation> p_list) |
IfMatchResult |
TacletMatcher.matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
Term p_template,
MatchConditions p_matchCond,
Services p_services)
Match the given template (which is probably a formula of the if
sequence) against a list of constraint formulas (probably the
formulas of the antecedent or the succedent), starting with the
given instantiations and constraint p_matchCond.
|
MatchConditions |
TacletMatcher.matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
MatchConditions p_matchCond,
Services p_services)
Match the whole if sequent using the given list of
instantiations of all if sequent formulas, starting with the
instantiations given by p_matchCond.
|
void |
IfFormulaInstantiationCache.put(boolean antec,
Semisequent s,
ImmutableList<IfFormulaInstantiation> value) |
protected TacletApp |
NoPosTacletApp.setAllInstantiations(MatchConditions mc,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services)
creates a new Taclet application containing all the
instantiations, constraints, new metavariables and if formula
instantiations given and forget the old ones
|
protected TacletApp |
PosTacletApp.setAllInstantiations(MatchConditions mc,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services)
creates a new Taclet application containing all the
instantiations, constraints, new metavariables and if formula
instantiations given and forget the old ones
|
protected abstract TacletApp |
TacletApp.setAllInstantiations(MatchConditions mc,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services)
creates a new Taclet application containing all the instantiations,
constraints, new metavariables and if formula instantiations given and
forget the old ones
|
TacletApp |
TacletApp.setIfFormulaInstantiations(ImmutableList<IfFormulaInstantiation> p_list,
Services p_services)
Creates a new Taclet application by matching the given formulas against
the formulas of the if sequent, adding SV instantiations, constraints and
metavariables as needed.
|
Constructor and Description |
---|
IfMatchResult(ImmutableList<IfFormulaInstantiation> p_candidates,
ImmutableList<MatchConditions> p_mcCandidates)
PRECONDITION: p_candidates.size () == p_mcCandidates.size ()
|
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<SequentChangeInfo> |
TacletExecutor.checkIfGoals(Goal p_goal,
ImmutableList<IfFormulaInstantiation> p_list,
MatchConditions p_matchCond,
int p_numberOfNewGoals)
Search for formulas within p_list that have to be proved by an
explicit assumes-goal, i.e.
|
Modifier and Type | Method and Description |
---|---|
IfMatchResult |
LegacyTacletMatcher.matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
Term p_template,
MatchConditions p_matchCond,
Services p_services)
(non-Javadoc)
|
MatchConditions |
LegacyTacletMatcher.matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
MatchConditions p_matchCond,
Services p_services) |
Modifier and Type | Method and Description |
---|---|
IfMatchResult |
VMTacletMatcher.matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
Term p_template,
MatchConditions p_matchCond,
Services p_services)
(non-Javadoc)
|
MatchConditions |
VMTacletMatcher.matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
MatchConditions p_matchCond,
Services p_services) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<IfFormulaInstantiation> |
IfInstantiationCachePool.IfInstantiationCache.get(boolean antec,
java.lang.Long key) |
Modifier and Type | Method and Description |
---|---|
void |
IfInstantiationCachePool.IfInstantiationCache.put(boolean antec,
java.lang.Long key,
ImmutableList<IfFormulaInstantiation> value) |
Copyright © 2003-2019 The KeY-Project.