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

Class NoFindTacletExecutor

java.lang.Object

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

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

All Implemented Interfaces:

RuleExecutor

public class NoFindTacletExecutor
extends TacletExecutor<NoFindTaclet>

Field Summary

Fields inherited from class de.uka.ilkd.key.rule.executor.javadl.TacletExecutor

taclet

Constructor Summary

Constructors

Constructor and Description
NoFindTacletExecutor(NoFindTaclet taclet)

Method Summary

Modifier and Type	Method and Description
ImmutableList<Goal>	apply(Goal goal, Services services, RuleApp ruleApp) the rule is applied on the given goal using the information of rule application.
protected void	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

Methods inherited from class de.uka.ilkd.key.rule.executor.javadl.TacletExecutor

addToAntec, addToSucc, applyAddProgVars, applyAddrule, checkIfGoals, instantiateSemisequent, replaceAtPos, syntacticalReplace

Methods inherited from class java.lang.Object

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

Constructor Detail

NoFindTacletExecutor

public NoFindTacletExecutor(NoFindTaclet taclet)

Method Detail

applyAdd

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

Parameters:

termLabelState - The TermLabelState of the current rule application.

add - the Sequent to be added

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

services - the Services encapsulating all java information

matchCond - the MatchConditions with all required instantiations

apply

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

the rule is applied on the given goal using the information of rule application.

Specified by:

apply in interface RuleExecutor

Specified by:

apply in class TacletExecutor<NoFindTaclet>

Parameters:

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

services - the Services encapsulating all java information

ruleApp - the taclet 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).