de.uka.ilkd.key.rule.executor.javadl

Class TacletExecutor<TacletKind extends Taclet>

java.lang.Object

de.uka.ilkd.key.rule.executor.javadl.TacletExecutor<TacletKind>

Type Parameters:

TacletKind - The kind of taclet that is executed.

All Implemented Interfaces:

RuleExecutor

Direct Known Subclasses:

FindTacletExecutor, NoFindTacletExecutor

public abstract class TacletExecutor<TacletKind extends Taclet>
extends java.lang.Object
implements RuleExecutor

Encapsulates the application engine of taclets.

Field Summary

Fields

Modifier and Type	Field and Description
private static java.lang.String	AUTONAME
protected TacletKind	taclet

Constructor Summary

Constructors

Constructor and Description
TacletExecutor(TacletKind taclet)

Method Summary

Modifier and Type	Method and Description
protected void	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).
private void	addToPos(Semisequent semi, TermLabelState termLabelState, SequentChangeInfo currentSequent, PosInOccurrence pos, PosInOccurrence applicationPosInOccurrence, boolean antec, Taclet.TacletLabelHint labelHint, MatchConditions matchCond, Goal goal, Services services, RuleApp tacletApp) instantiates the constrained formulas of semisequent semi and adds the instantiatied formulas at the specified position to goal
private void	addToPosWithoutInst(SequentFormula frm, SequentChangeInfo currentSequent, PosInOccurrence pos, boolean antec) adds SequentFormula to antecedent or succedent depending on position information or the boolean antec contrary to "addToPos" frm will not be modified
protected void	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).
abstract ImmutableList<Goal>	apply(Goal goal, Services services, RuleApp tacletApp) applies the given rule application to the specified goal
protected void	applyAddProgVars(ImmutableSet<SchemaVariable> pvs, SequentChangeInfo currentSequent, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)
protected void	applyAddrule(ImmutableList<Taclet> rules, Goal goal, Services services, MatchConditions matchCond) adds the given rules (i.e. the rules to add according to the Taclet goal template to the node of the given goal
protected ImmutableList<SequentChangeInfo>	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. elements of type IfFormulaInstDirect.
private SequentFormula	instantiateReplacement(TermLabelState termLabelState, SequentFormula schemaFormula, Services services, MatchConditions matchCond, PosInOccurrence applicationPosInOccurrence, Taclet.TacletLabelHint labelHint, Goal goal, RuleApp tacletApp) the given constrained formula is instantiated and then the result (usually a complete instantiated formula) is returned.
protected ImmutableList<SequentFormula>	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	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	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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

AUTONAME

private static final java.lang.String AUTONAME

See Also:

Constant Field Values

taclet

protected final TacletKind extends Taclet taclet

Constructor Detail

TacletExecutor

public TacletExecutor(TacletKind taclet)

Method Detail

apply

public abstract ImmutableList<Goal> apply(Goal goal,
                                          Services services,
                                          RuleApp tacletApp)

applies the given rule application to the specified goal

Specified by:

apply in interface RuleExecutor

Parameters:

goal - the goal that the rule application should refer to.

services - the Services encapsulating all java information

tacletApp - the rule application that is executed.

Returns:

List of the goals created by the rule which have to be proved. If this is a close-goal-taclet ( this.closeGoal () ), the first goal of the return list is the goal that should be closed (with the constraint this taclet is applied under).

syntacticalReplace

protected Term 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

Parameters:

term - the Term the syntactical replacement is performed on

termLabelState - The TermLabelState of the current rule application.

labelHint - the hint used to maintain TermLabels.

applicationPosInOccurrence - the PosInOccurrence of the find term in the sequent this taclet is applied to

mc - the MatchConditions with all instantiations and the constraint

goal - the Goal on which this taclet is applied

ruleApp - the RuleApp with application information

services - the Services with the Java model information

Returns:

the (partially) instantiated term

addToPosWithoutInst

private void addToPosWithoutInst(SequentFormula frm,
                                 SequentChangeInfo currentSequent,
                                 PosInOccurrence pos,
                                 boolean antec)

adds SequentFormula to antecedent or succedent depending on position information or the boolean antec contrary to "addToPos" frm will not be modified

Parameters:

frm - the SequentFormula that should be added

currentSequent - the SequentChangeInfo which is the current (intermediate) result of applying the taclet

pos - the PosInOccurrence describing the place in the sequent

antec - boolean true(false) if elements have to be added to the antecedent(succedent) (only looked at if pos == null)

instantiateReplacement

private SequentFormula instantiateReplacement(TermLabelState termLabelState,
                                              SequentFormula schemaFormula,
                                              Services services,
                                              MatchConditions matchCond,
                                              PosInOccurrence applicationPosInOccurrence,
                                              Taclet.TacletLabelHint labelHint,
                                              Goal goal,
                                              RuleApp tacletApp)

the given constrained formula is instantiated and then the result (usually a complete instantiated formula) is returned.

Parameters:

termLabelState - The TermLabelState of the current rule application.

schemaFormula - the SequentFormula to be instantiated

services - the Services object carrying ja related information

matchCond - the MatchConditions object with the instantiations of the schemavariables, constraints etc.

applicationPosInOccurrence - The PosInOccurrence of the Term which is rewritten

labelHint - The hint used to maintain TermLabels.

Returns:

the as far as possible instantiated SequentFormula

instantiateSemisequent

protected ImmutableList<SequentFormula> 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

Parameters:

semi - the Semisequent to be instantiated

termLabelState - The TermLabelState of the current rule application.

labelHint - The hint used to maintain TermLabels.

applicationPosInOccurrence - The PosInOccurrence of the Term which is rewritten

matchCond - the MatchConditions including the mapping Schemavariables to concrete logic elements

services - the Services

Returns:

the instantiated formulas of the semisequent as list

replaceAtPos

protected void 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

Parameters:

semi - the Semisequent with the the ConstrainedFormulae to be added

termLabelState - The TermLabelState of the current rule application.

currentSequent - the Sequent which is the current (intermediate) result of applying the taclet

pos - the PosInOccurrence describing the place in the sequent

matchCond - the MatchConditions containing in particular

labelHint - The hint used to maintain TermLabels. the instantiations of the schemavariables

services - the Services encapsulating all java information

addToPos

private void addToPos(Semisequent semi,
                      TermLabelState termLabelState,
                      SequentChangeInfo currentSequent,
                      PosInOccurrence pos,
                      PosInOccurrence applicationPosInOccurrence,
                      boolean antec,
                      Taclet.TacletLabelHint labelHint,
                      MatchConditions matchCond,
                      Goal goal,
                      Services services,
                      RuleApp tacletApp)

instantiates the constrained formulas of semisequent semi and adds the instantiatied formulas at the specified position to goal

Parameters:

semi - the Semisequent with the the ConstrainedFormulae to be added

termLabelState - The TermLabelState of the current rule application.

currentSequent - the Sequent which is the current (intermediate) result of applying the taclet

pos - the PosInOccurrence describing the place in the sequent

applicationPosInOccurrence - The PosInOccurrence of the Term which is rewritten

antec - boolean true(false) if elements have to be added to the antecedent(succedent) (only looked at if pos == null)

labelHint - The hint used to maintain TermLabels. the instantiations of the schemavariables

matchCond - the MatchConditions containing in particular

services - the Services encapsulating all java information

addToAntec

protected void 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). Of course it has to be ensured that the position information describes one occurrence in the antecedent of the sequent.

Parameters:

semi - the Semisequent with the the ConstrainedFormulae to be added

termLabelState - The TermLabelState of the current rule application.

labelHint - The hint used to maintain TermLabels.

currentSequent - the Sequent which is the current (intermediate) result of applying the taclet

pos - the PosInOccurrence describing the place in the sequent or null for head of antecedent

applicationPosInOccurrence - The PosInOccurrence of the Term which is rewritten

matchCond - the MatchConditions containing in particular the instantiations of the schemavariables

services - the Services encapsulating all java information

addToSucc

protected void 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). Of course it has to be ensured that the position information describes one occurrence in the succedent of the sequent.

Parameters:

semi - the Semisequent with the the ConstrainedFormulae to be added

termLabelState - The TermLabelState of the current rule application.

labelHint - The hint used to maintain TermLabels.

pos - the PosInOccurrence describing the place in the sequent or null for head of antecedent

applicationPosInOccurrence - The PosInOccurrence of the Term which is rewritten

matchCond - the MatchConditions containing in particular the instantiations of the schemavariables

goal - the Goal that knows the node the formulae have to be added

services - the Services encapsulating all java information

applyAddrule

protected void applyAddrule(ImmutableList<Taclet> rules,
                            Goal goal,
                            Services services,
                            MatchConditions matchCond)

adds the given rules (i.e. the rules to add according to the Taclet goal template to the node of the given goal

Parameters:

rules - the rules to be added

goal - the goal describing the node where the rules should be added

services - the Services encapsulating all java information

matchCond - the MatchConditions containing in particular the instantiations of the schemavariables

applyAddProgVars

protected void applyAddProgVars(ImmutableSet<SchemaVariable> pvs,
                                SequentChangeInfo currentSequent,
                                Goal goal,
                                PosInOccurrence posOfFind,
                                Services services,
                                MatchConditions matchCond)

checkIfGoals

protected ImmutableList<SequentChangeInfo> 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. elements of type IfFormulaInstDirect.

Parameters:

p_goal - the Goal on which the taclet is applied

p_list - the list of IfFormulaInstantiation containing the instantiations for the assumes formulas

p_matchCond - the MatchConditions with the instantiations of the schema variables

p_numberOfNewGoals - the number of new goals the Taclet creates in any case because of existing TacletGoalTemplates

Returns:

a list with the original sequent if no such formulas existed, otherwise the list has two entries: one for the original sequent and one with the sequent encoding the proof obligation for the to be proven formulas of the assumes goal