Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
de.uka.ilkd.key.informationflow.rule.executor | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
de.uka.ilkd.key.java.expression |
Elements of the Java syntax tree representing expressions.
|
de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.conditions | |
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.rule.match.vm.instructions |
Modifier and Type | Field and Description |
---|---|
MatchConditions |
SearchNode.mc |
Constructor and Description |
---|
SearchNode(SearchNode parent,
MatchConditions cond) |
Modifier and Type | Method and Description |
---|---|
protected void |
InfFlowContractAppTacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
JavaNonTerminalProgramElement.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
CcatchReturnValParameterDeclaration.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
JavaProgramElement.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
ContextStatementBlock.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
ProgramElement.match(SourceData source,
MatchConditions matchCond)
matches the source "text" (@link SourceData#getSource()) against the pattern represented
by this object.
|
protected MatchConditions |
JavaNonTerminalProgramElement.matchChildren(SourceData source,
MatchConditions matchCond,
int offset)
matches successively all children of this current node.
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
JavaNonTerminalProgramElement.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
CcatchReturnValParameterDeclaration.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
JavaProgramElement.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
ContextStatementBlock.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
ProgramElement.match(SourceData source,
MatchConditions matchCond)
matches the source "text" (@link SourceData#getSource()) against the pattern represented
by this object.
|
protected MatchConditions |
JavaNonTerminalProgramElement.matchChildren(SourceData source,
MatchConditions matchCond,
int offset)
matches successively all children of this current node.
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
VariableSpecification.match(SourceData source,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
VariableSpecification.match(SourceData source,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
Literal.match(SourceData source,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
Literal.match(SourceData source,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
SchemaTypeReference.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
TypeReferenceImp.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
SchematicFieldReference.match(SourceData source,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
SchemaTypeReference.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
TypeReferenceImp.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
SchematicFieldReference.match(SourceData source,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
TransactionStatement.match(SourceData source,
MatchConditions conditions) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
TransactionStatement.match(SourceData source,
MatchConditions conditions) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
ProgramElementName.match(SourceData source,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
ProgramElementName.match(SourceData source,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
ProgramVariable.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
ProgramMethod.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
ProgramSV.match(SourceData source,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
ProgramVariable.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
ProgramMethod.match(SourceData source,
MatchConditions matchCond) |
MatchConditions |
ProgramSV.match(SourceData source,
MatchConditions matchCond) |
Modifier and Type | Field and Description |
---|---|
static MatchConditions |
MatchConditions.EMPTY_MATCHCONDITIONS |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
MatchConditions.addRenaming(QuantifiableVariable q1,
QuantifiableVariable q2) |
MatchConditions |
VariableConditionAdapter.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
VariableCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
MatchConditions |
TacletMatcher.checkConditions(MatchConditions p_matchconditions,
Services services)
checks the provided matches against the variable conditions of this taclet
It returns the resulting match conditions or
null if the found matches
do not satisfy the variable conditions. |
MatchConditions |
RewriteTaclet.checkPrefix(PosInOccurrence p_pos,
MatchConditions p_mc)
For taclets with
getSameUpdatePrefix () , collect
the updates above p_pos and add them to the update
context of the instantiations object p_mc . |
MatchConditions |
TacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
MatchConditions |
MatchConditions.extendRenameTable() |
MatchConditions |
TacletApp.matchConditions() |
MatchConditions |
TacletMatcher.matchFind(Term term,
MatchConditions matchCond,
Services services)
matches the given term against the taclet's find term
if the taclet has no find term or the match is unsuccessful
null
is returned |
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.
|
MatchConditions |
TacletMatcher.matchSV(SchemaVariable sv,
ProgramElement term,
MatchConditions matchCond,
Services services)
|
MatchConditions |
TacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
MatchConditions |
MatchConditions.setInstantiations(SVInstantiations p_instantiations) |
protected MatchConditions |
NoPosTacletApp.setupMatchConditions(PosInOccurrence pos,
TermServices services) |
MatchConditions |
MatchConditions.shrinkRenameTable() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<MatchConditions> |
IfMatchResult.getMatchConditions() |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
VariableConditionAdapter.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
VariableCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
MatchConditions |
TacletMatcher.checkConditions(MatchConditions p_matchconditions,
Services services)
checks the provided matches against the variable conditions of this taclet
It returns the resulting match conditions or
null if the found matches
do not satisfy the variable conditions. |
MatchConditions |
RewriteTaclet.checkPrefix(PosInOccurrence p_pos,
MatchConditions p_mc)
For taclets with
getSameUpdatePrefix () , collect
the updates above p_pos and add them to the update
context of the instantiations object p_mc . |
MatchConditions |
TacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
MatchConditions matchCond,
Services services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
MatchConditions matchCond,
PosInOccurrence pos,
Services services) |
MatchConditions |
TacletMatcher.matchFind(Term term,
MatchConditions matchCond,
Services services)
matches the given term against the taclet's find term
if the taclet has no find term or the match is unsuccessful
null
is returned |
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.
|
MatchConditions |
TacletMatcher.matchSV(SchemaVariable sv,
ProgramElement term,
MatchConditions matchCond,
Services services)
|
MatchConditions |
TacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
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 |
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
|
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 |
---|---|
MatchConditions |
FieldTypeToSortCondition.check(SchemaVariable var,
SVSubstitute svSubst,
MatchConditions matchCond,
Services services) |
MatchConditions |
DropEffectlessElementariesCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
NewJumpLabelCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
IsLabeledCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
SimplifyIfThenElseUpdateCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
LoopVariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
StoreStmtInCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
ObserverCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
HasLoopInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
LoopFreeInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
EqualUniqueCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
ApplyUpdateOnRigidCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
JavaTypeToSortCondition.check(SchemaVariable var,
SVSubstitute svSubst,
MatchConditions matchCond,
Services services) |
MatchConditions |
LoopInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
DropEffectlessStoresCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
StoreTermInCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
SameObserverCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected void |
TacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
adds SequentFormula to antecedent depending on
position information (if none is handed over it is added at the
head of the antecedent).
|
protected void |
TacletExecutor.addToSucc(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds SequentFormula to succedent depending on
position information (if none is handed over it is added at the
head of the succedent).
|
protected void |
RewriteTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
SuccTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
NoFindTacletExecutor.applyAdd(TermLabelState termLabelState,
Sequent add,
SequentChangeInfo currentSequent,
Services services,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
TacletExecutor.applyAddProgVars(ImmutableSet<SchemaVariable> pvs,
SequentChangeInfo currentSequent,
Goal goal,
PosInOccurrence posOfFind,
Services services,
MatchConditions matchCond) |
protected void |
TacletExecutor.applyAddrule(ImmutableList<Taclet> rules,
Goal goal,
Services services,
MatchConditions matchCond)
adds the given rules (i.e.
|
protected void |
RewriteTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
SuccTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
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.
|
protected ImmutableList<SequentFormula> |
TacletExecutor.instantiateSemisequent(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
instantiates the given semisequent with the instantiations found in
Matchconditions
|
protected void |
TacletExecutor.replaceAtPos(Semisequent semi,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
MatchConditions matchCond,
Taclet.TacletLabelHint labelHint,
Goal goal,
RuleApp ruleApp,
Services services)
replaces the constrained formula at the given position with the first
formula in the given semisequent and adds possible other formulas of the
semisequent starting at the position
|
protected Term |
TacletExecutor.syntacticalReplace(Term term,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions mc,
Goal goal,
RuleApp ruleApp,
Services services)
a new term is created by replacing variables of term whose replacement is
found in the given SVInstantiations
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
LegacyTacletMatcher.checkConditions(MatchConditions cond,
Services services)
checks the provided matches against the variable conditions of this taclet
It returns the resulting match conditions or
null if the found matches
do not satisfy the variable conditions. |
MatchConditions |
LegacyTacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
abstract MatchConditions |
ElementMatcher.match(T op,
SVSubstitute subst,
MatchConditions mc,
Services services) |
MatchConditions |
LegacyTacletMatcher.matchFind(Term term,
MatchConditions matchCond,
Services services)
matches the given term against the taclet's find term
if the taclet has no find term or the match is unsuccessful
null
is returned |
MatchConditions |
LegacyTacletMatcher.matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
MatchConditions p_matchCond,
Services p_services) |
protected MatchConditions |
LegacyTacletMatcher.matchJavaBlock(Term term,
Term template,
MatchConditions matchCond,
Services services)
returns the matchconditions that are required if the java block of the
given term matches the schema given by the template term or null if no
match is possible
(marked as final to help the compiler inlining methods)
|
MatchConditions |
LegacyTacletMatcher.matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
MatchConditions |
LegacyTacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
LegacyTacletMatcher.checkConditions(MatchConditions cond,
Services services)
checks the provided matches against the variable conditions of this taclet
It returns the resulting match conditions or
null if the found matches
do not satisfy the variable conditions. |
MatchConditions |
LegacyTacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
abstract MatchConditions |
ElementMatcher.match(T op,
SVSubstitute subst,
MatchConditions mc,
Services services) |
MatchConditions |
LegacyTacletMatcher.matchFind(Term term,
MatchConditions matchCond,
Services services)
matches the given term against the taclet's find term
if the taclet has no find term or the match is unsuccessful
null
is returned |
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) |
protected MatchConditions |
LegacyTacletMatcher.matchJavaBlock(Term term,
Term template,
MatchConditions matchCond,
Services services)
returns the matchconditions that are required if the java block of the
given term matches the schema given by the template term or null if no
match is possible
(marked as final to help the compiler inlining methods)
|
MatchConditions |
LegacyTacletMatcher.matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
MatchConditions |
LegacyTacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
VMTacletMatcher.checkConditions(MatchConditions cond,
Services services)
checks the provided matches against the variable conditions of this taclet
It returns the resulting match conditions or
null if the found matches
do not satisfy the variable conditions. |
MatchConditions |
VMTacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
MatchConditions |
TacletMatchProgram.match(Term p_toMatch,
MatchConditions p_matchCond,
Services services)
executes the program and tries to match the provided term; additional restrictions are provided via match conditions.
|
MatchConditions |
VMTacletMatcher.matchFind(Term term,
MatchConditions matchCond,
Services services)
matches the given term against the taclet's find term
if the taclet has no find term or the match is unsuccessful
null
is returned |
MatchConditions |
VMTacletMatcher.matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
MatchConditions p_matchCond,
Services p_services) |
MatchConditions |
VMTacletMatcher.matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
MatchConditions |
VMTacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
VMTacletMatcher.checkConditions(MatchConditions cond,
Services services)
checks the provided matches against the variable conditions of this taclet
It returns the resulting match conditions or
null if the found matches
do not satisfy the variable conditions. |
MatchConditions |
VMTacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
MatchConditions |
TacletMatchProgram.match(Term p_toMatch,
MatchConditions p_matchCond,
Services services)
executes the program and tries to match the provided term; additional restrictions are provided via match conditions.
|
MatchConditions |
VMTacletMatcher.matchFind(Term term,
MatchConditions matchCond,
Services services)
matches the given term against the taclet's find term
if the taclet has no find term or the match is unsuccessful
null
is returned |
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) |
MatchConditions |
VMTacletMatcher.matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
MatchConditions |
VMTacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Method and Description |
---|---|
protected MatchConditions |
MatchProgramSVInstruction.addInstantiation(ProgramElement pe,
MatchConditions matchCond,
Services services)
tries to add the pair (this,pe) to the match conditions.
|
protected MatchConditions |
MatchSchemaVariableInstruction.addInstantiation(Term term,
MatchConditions matchCond,
Services services)
Tries to add the pair (this,term) to the match conditions.
|
MatchConditions |
MatchProgramSVInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOperatorInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOpIdentityInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchProgramSVInstruction.match(ProgramElement instantiationCandidate,
MatchConditions matchCond,
Services services)
tries to match the schema variable of this instruction with the specified
ProgramElement instantiationCandidate
w.r.t. |
MatchConditions |
MatchSchemaVariableInstruction.match(ProgramElement instantiationCandidate,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
ProgramElement instantiationCandidate
w.r.t. |
MatchConditions |
MatchUpdateSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchProgramSVInstruction.match(Term instantiationCandidate,
MatchConditions matchCond,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchFormulaSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchElementaryUpdateInstruction.match(Term instantiationCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
MatchModalOperatorSVInstruction.match(Term subst,
MatchConditions mc,
Services services) |
abstract MatchConditions |
Instruction.match(Term instantiationCandidate,
MatchConditions matchCond,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchOpIdentityInstruction.match(Term instantiationCandidate,
MatchConditions matchConditions,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchTermSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchVariableSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchSortDependingFunctionInstruction.match(Term instantiationCandidate,
MatchConditions matchConditions,
Services services)
Tries to match the top level operator of the given term with this instruction's sort depending function symbol.
|
MatchConditions |
MatchUpdateSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchProgramSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchFormulaSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchElementaryUpdateInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchModalOperatorSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchProgramInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchTermLabelInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOpIdentityInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchTermSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchVariableSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
UnbindVariablesInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchSortDependingFunctionInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
BindVariablesInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected MatchConditions |
MatchProgramSVInstruction.addInstantiation(ProgramElement pe,
MatchConditions matchCond,
Services services)
tries to add the pair (this,pe) to the match conditions.
|
protected MatchConditions |
MatchSchemaVariableInstruction.addInstantiation(Term term,
MatchConditions matchCond,
Services services)
Tries to add the pair (this,term) to the match conditions.
|
MatchConditions |
MatchProgramSVInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOperatorInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOpIdentityInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchProgramSVInstruction.match(ProgramElement instantiationCandidate,
MatchConditions matchCond,
Services services)
tries to match the schema variable of this instruction with the specified
ProgramElement instantiationCandidate
w.r.t. |
MatchConditions |
MatchSchemaVariableInstruction.match(ProgramElement instantiationCandidate,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
ProgramElement instantiationCandidate
w.r.t. |
MatchConditions |
MatchUpdateSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchProgramSVInstruction.match(Term instantiationCandidate,
MatchConditions matchCond,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchFormulaSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchElementaryUpdateInstruction.match(Term instantiationCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
MatchModalOperatorSVInstruction.match(Term subst,
MatchConditions mc,
Services services) |
abstract MatchConditions |
Instruction.match(Term instantiationCandidate,
MatchConditions matchCond,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchOpIdentityInstruction.match(Term instantiationCandidate,
MatchConditions matchConditions,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchTermSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchVariableSVInstruction.match(Term subst,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
Term instantiationCandidate
w.r.t. |
MatchConditions |
MatchSortDependingFunctionInstruction.match(Term instantiationCandidate,
MatchConditions matchConditions,
Services services)
Tries to match the top level operator of the given term with this instruction's sort depending function symbol.
|
MatchConditions |
MatchUpdateSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchProgramSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchFormulaSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchElementaryUpdateInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchModalOperatorSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchProgramInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchTermLabelInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOpIdentityInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchTermSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchVariableSVInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
UnbindVariablesInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchSortDependingFunctionInstruction.match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
MatchConditions |
MatchInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
MatchConditions |
BindVariablesInstruction.match(TermNavigator termPosition,
MatchConditions matchConditions,
Services services) |
Copyright © 2003-2019 The KeY-Project.