de.uka.ilkd.key.rule.executor

Interface RuleExecutor

All Known Implementing Classes:

AntecTacletExecutor, FindTacletExecutor, InfFlowContractAppTacletExecutor, NoFindTacletExecutor, RewriteTacletExecutor, SuccTacletExecutor, TacletExecutor

public interface RuleExecutor

Executes a Rule with respect to a given instantiation of the schemavariables.

Method Summary

Modifier and Type	Method and Description
ImmutableList<Goal>	apply(Goal goal, Services services, RuleApp ruleApp) applies the given rule application to the specified goal

Method Detail

apply

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

applies the given rule application to the specified goal

Parameters:

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

services - the Services encapsulating all java information

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