Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.control.instantiation_model | |
de.uka.ilkd.key.gui.nodeviews | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
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.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.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.strategy.feature | |
de.uka.ilkd.key.strategy.feature.findprefix | |
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.util |
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<TacletApp> |
AbstractProofControl.getAppsForName(Goal goal,
java.lang.String name,
PosInOccurrence pos)
collects all Taclet applications at the given position of the specified
taclet
|
protected ImmutableSet<TacletApp> |
AbstractProofControl.getAppsForName(Goal goal,
java.lang.String name,
PosInOccurrence pos,
TacletFilter filter)
collects all taclet applications for the given position and taclet
(identified by its name) matching the filter condition
|
ImmutableList<TacletApp> |
AbstractProofControl.getFindTaclet(Goal focusedGoal,
PosInOccurrence pos) |
ImmutableList<TacletApp> |
ProofControl.getFindTaclet(Goal focusedGoal,
PosInOccurrence pos)
collects all applicable FindTaclets of the current goal (called by the
SequentViewer)
|
ImmutableList<TacletApp> |
AbstractProofControl.getNoFindTaclet(Goal focusedGoal) |
ImmutableList<TacletApp> |
ProofControl.getNoFindTaclet(Goal focusedGoal)
collects all applicable NoFindTaclets of the current goal (called by the
SequentViewer)
|
ImmutableList<TacletApp> |
AbstractProofControl.getRewriteTaclet(Goal focusedGoal,
PosInOccurrence pos) |
ImmutableList<TacletApp> |
ProofControl.getRewriteTaclet(Goal focusedGoal,
PosInOccurrence pos)
collects all applicable RewriteTaclets of the current goal (called by the
SequentViewer)
|
Modifier and Type | Method and Description |
---|---|
TacletInstantiationModel |
AbstractProofControl.createModel(TacletApp app,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
TacletInstantiationModel[] |
AbstractProofControl.completeAndApplyApp(java.util.List<TacletApp> apps,
Goal goal) |
boolean |
AbstractProofControl.selectedTaclet(ImmutableSet<TacletApp> applics,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
TacletApp |
TacletInstantiationModel.application() |
TacletApp |
TacletInstantiationModel.createTacletApp() |
TacletApp |
TacletFindModel.createTacletAppFromVarInsts() |
TacletApp |
TacletInstantiationModel.tacletApp() |
Constructor and Description |
---|
TacletAssumesModel(Term ifFma,
ImmutableList<IfFormulaInstantiation> candidates,
TacletApp app,
Goal goal,
Services services,
NamespaceSet nss,
AbbrevMap scm) |
TacletFindModel(TacletApp app,
Services services,
NamespaceSet nss,
AbbrevMap scm,
Goal goal)
Create new data model for tree.
|
TacletInstantiationModel(TacletApp app,
Sequent seq,
NamespaceSet nss,
AbbrevMap scm,
Goal goal)
Create new data model for the apply Taclet dialog wrapping a combo box model
and a table model.
|
Modifier and Type | Method and Description |
---|---|
TacletApp |
InsertionTacletBrowserMenuItem.connectedTo() |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<TacletApp> |
CurrentGoalViewMenu.removeRewrites(ImmutableList<TacletApp> list)
removes RewriteTaclet from list
|
static ImmutableList<TacletApp> |
CurrentGoalViewMenu.sort(ImmutableList<TacletApp> finds,
CurrentGoalViewMenu.TacletAppComparator comp)
This method is also used by the KeYIDE has to be static and public.
|
Modifier and Type | Method and Description |
---|---|
void |
InsertionTacletBrowserMenuItem.add(TacletApp app)
Adds a new taclet to be displayed by this component
it is assumed that the app has been tested before by
InsertionTacletBrowserMenuItem.isResponsible(de.uka.ilkd.key.rule.Taclet) . |
int |
CurrentGoalViewMenu.TacletAppComparator.compare(TacletApp o1,
TacletApp o2) |
de.uka.ilkd.key.gui.nodeviews.InsertionTacletBrowserMenuItem.TacletAppListItem |
InsertSystemInvariantTacletMenuItem.createListItem(TacletApp app) |
de.uka.ilkd.key.gui.nodeviews.InsertionTacletBrowserMenuItem.TacletAppListItem |
InsertionTacletBrowserMenuItem.createListItem(TacletApp app) |
java.util.LinkedHashMap<java.lang.String,java.lang.Integer> |
CurrentGoalViewMenu.TacletAppComparator.score(TacletApp o1) |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<TacletApp> |
CurrentGoalViewMenu.removeRewrites(ImmutableList<TacletApp> list)
removes RewriteTaclet from list
|
static ImmutableList<TacletApp> |
CurrentGoalViewMenu.sort(ImmutableList<TacletApp> finds,
CurrentGoalViewMenu.TacletAppComparator comp)
This method is also used by the KeYIDE has to be static and public.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
VariableNamer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
|
java.lang.String |
VariableNamer.getSuggestiveNameProposalForProgramVariable(SchemaVariable sv,
TacletApp app,
Services services,
ImmutableList<java.lang.String> previousProposals) |
Modifier and Type | Method and Description |
---|---|
java.util.List<TacletApp> |
Goal.getAllTacletApps(Services services) |
ImmutableList<TacletApp> |
TacletAppIndex.getTacletAppAt(PosInOccurrence pos,
TacletFilter filter,
Services services)
returns the set of rule applications
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
RuleAppIndex.getTacletAppAt(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the set of rule applications for
the given heuristics
at the given position of the given sequent.
|
ImmutableList<TacletApp> |
TermTacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
ImmutableList<TacletApp> |
SemisequentTacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
RuleFilter filter,
Services services) |
ImmutableList<TacletApp> |
TacletAppIndex.getTacletAppAtAndBelow(PosInOccurrence pos,
TacletFilter filter,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
ImmutableList<TacletApp> |
RuleAppIndex.getTacletAppAtAndBelow(TacletFilter filter,
PosInOccurrence pos,
Services services)
returns the rule applications at the given PosInOccurrence and at all
Positions below this.
|
Modifier and Type | Method and Description |
---|---|
protected static java.lang.String |
VariableNameProposer.createBaseNameProposalBasedOnCorrespondence(TacletApp p_app,
SchemaVariable p_var,
Services services)
Find a name for the variable
p_var , based on the result
of Taclet.getNameCorrespondent |
java.lang.String |
InstantiationProposer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
Returns an instantiation proposal for the schema variable var.
|
java.lang.String |
VariableNameProposer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
Returns an instantiation proposal for the schema variable var.
|
java.lang.String |
InstantiationProposerCollection.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals) |
Modifier and Type | Method and Description |
---|---|
static TacletApp |
IntermediateProofReplayer.parseSV1(TacletApp app,
SchemaVariable sv,
java.lang.String value,
Services services)
Instantiates a schema variable in the given taclet application.
|
static TacletApp |
IntermediateProofReplayer.parseSV2(TacletApp app,
SchemaVariable sv,
java.lang.String value,
Goal targetGoal)
Instantiates a schema variable in the given taclet application.
|
Modifier and Type | Method and Description |
---|---|
static TacletApp |
IntermediateProofReplayer.parseSV1(TacletApp app,
SchemaVariable sv,
java.lang.String value,
Services services)
Instantiates a schema variable in the given taclet application.
|
static TacletApp |
IntermediateProofReplayer.parseSV2(TacletApp app,
SchemaVariable sv,
java.lang.String value,
Goal targetGoal)
Instantiates a schema variable in the given taclet application.
|
Modifier and Type | Class and Description |
---|---|
class |
NoPosTacletApp
A no position taclet application has no position information yet.
|
class |
PosTacletApp
A position taclet application object, contains already the information to
which term/formula of the sequent the taclet is attached.
|
Modifier and Type | Method and Description |
---|---|
TacletApp |
TacletApp.addCheckedInstantiation(SchemaVariable sv,
ProgramElement pe,
Services services,
boolean interesting)
checks if the instantiation of
sv with pe is
possible. |
TacletApp |
TacletApp.addCheckedInstantiation(SchemaVariable sv,
Term term,
Services services,
boolean interesting)
creates a new Tacletapp where the SchemaVariable sv is instantiated with
the the given Term term.
|
TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
Name name,
Services services) |
TacletApp |
NoPosTacletApp.addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
TacletApp |
PosTacletApp.addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
abstract TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
TacletApp |
NoPosTacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
PosTacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
abstract TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp.
|
TacletApp |
NoPosTacletApp.addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
PosTacletApp.addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
abstract TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
NoPosTacletApp.addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and hold the old ones
|
TacletApp |
PosTacletApp.addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and the ones of this TacletApp
|
abstract TacletApp |
TacletApp.addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the instantiations given
by the SVInstantiations
|
TacletApp |
TacletApp.createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
boolean interesting,
Services services)
Create a new constant named "instantiation" and instantiate "sv" with.
|
TacletApp |
TacletApp.createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
Sort sort,
boolean interesting,
Services services) |
TacletApp |
TacletApp.prepareUserInstantiation(Services services)
checks if there are name conflicts (i.e.
|
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.
|
protected TacletApp |
NoPosTacletApp.setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and forget the ones in this TacletApp
|
protected TacletApp |
PosTacletApp.setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and forget the old ones.
|
protected abstract TacletApp |
TacletApp.setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the instantiations given
by the SVInstantiations and forget the old ones
|
TacletApp |
NoPosTacletApp.setMatchConditions(MatchConditions mc,
Services services)
creates a new Taclet application containing all the
instantiations, constraints and new metavariables given
by the mc object and forget the old ones
|
TacletApp |
PosTacletApp.setMatchConditions(MatchConditions mc,
Services services)
creates a new Taclet application containing all the
instantiations, constraints and new metavariables given
by the mc object and forget the old ones
|
abstract TacletApp |
TacletApp.setMatchConditions(MatchConditions mc,
Services services)
creates a new Taclet application containing all the instantiations,
constraints and new metavariables given by the mc object and forget the
old ones
|
TacletApp |
TacletApp.tryToInstantiate(Services services) |
TacletApp |
TacletApp.tryToInstantiateAsMuchAsPossible(Services services) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<TacletApp> |
TacletApp.findIfFormulaInstantiations(Sequent p_seq,
Services p_services)
Find all possible instantiations of the if sequent formulas within the
sequent "p_seq".
|
Modifier and Type | Method and Description |
---|---|
SequentFormula |
RewriteTaclet.getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
Modifier and Type | Method and Description |
---|---|
SequentFormula |
RewriteTacletExecutor.getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
Modifier and Type | Method and Description |
---|---|
TacletApp |
TacletAppContainer.completeRuleApp(Goal p_goal)
Create a
RuleApp that is suitable to be applied
or null . |
Modifier and Type | Method and Description |
---|---|
protected boolean |
IntroducedSymbolBy.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
NonDuplicateAppFeature.comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio) |
protected boolean |
NonDuplicateAppModPositionFeature.comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio) |
protected boolean |
EqNonDuplicateAppFeature.comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio) |
protected boolean |
InfFlowContractAppFeature.comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio)
Compare whether two
PosInOccurrence s are equal. |
protected abstract boolean |
AbstractNonDuplicateAppFeature.comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio)
Compare whether two
PosInOccurrence s are equal. |
protected boolean |
NonDuplicateAppFeature.containsRuleApp(ImmutableList<RuleApp> list,
TacletApp rapp,
PosInOccurrence pio) |
protected boolean |
InfFlowContractAppFeature.duplicateFindTaclet(TacletApp app,
PosInOccurrence pos,
Goal goal)
Search for a duplicate of the application
app by walking upwards in the proof tree. |
protected boolean |
TriggerVarInstantiatedFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
SetsSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
MatchedIfFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
TacletRequiringInstantiationFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
OnlyInScopeOfQuantifiersFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
InEquationMultFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
AutomatedRuleFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
MonomialsSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
ReducibleMonomialsFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
TopLevelFindFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
TermSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
NoSelfApplicationFeature.filter(TacletApp p_app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
DiffFindAndIfFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
AtomsSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected abstract boolean |
BinaryTacletAppFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
protected boolean |
SVNeedsInstantiation.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
NonDuplicateAppFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
PolynomialValuesCmpFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
TrivialMonomialLCRFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
NonDuplicateAppModPositionFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
EqNonDuplicateAppFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
DiffFindAndReplacewithFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
InstantiatedSVFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
CheckApplyEqFeature.filter(TacletApp p_app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
AbstractNonDuplicateAppFeature.noDuplicateFindTaclet(TacletApp app,
PosInOccurrence pos,
Goal goal)
Search for a duplicate of the application
app by walking
upwards in the proof tree. |
protected boolean |
InfFlowContractAppFeature.sameApplication(RuleApp ruleCmp,
TacletApp newApp,
PosInOccurrence newPio)
Check whether the old rule application
ruleCmp is a duplicate of the new application
newApp at position
newPio .newPio can be
null |
protected boolean |
AbstractNonDuplicateAppFeature.sameApplication(RuleApp ruleCmp,
TacletApp newApp,
PosInOccurrence newPio)
Check whether the old rule application
ruleCmp is a
duplicate of the new application newApp at position
newPio .newPio can be null |
Modifier and Type | Method and Description |
---|---|
protected boolean |
FindPrefixRestrictionFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
LiteralsSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
ClausesSmallerThanFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
ExistentiallyConnectedFormulasFeature.filter(TacletApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected static void |
TruthValueTracingUtil.analyzeTacletGoal(Node parent,
TacletApp tacletApp,
TacletGoalTemplate tacletGoal,
java.util.List<de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil.LabelOccurrence> labels,
Services services,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Analyzes the given
TacletGoalTemplate . |
protected static java.util.List<de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil.LabelOccurrence> |
TruthValueTracingUtil.findInvolvedLabels(Sequent sequent,
TacletApp tacletApp,
Name termLabelName)
Computes the occurrences of all involved
FormulaTermLabel s. |
Modifier and Type | Method and Description |
---|---|
static Term |
SymbolicExecutionUtil.instantiateTerm(Node node,
Term term,
TacletApp tacletApp,
Services services)
|
Copyright © 2003-2019 The KeY-Project.