de.uka.ilkd.key.rule

Interface Rule

All Known Subinterfaces:

BuiltInRule

All Known Implementing Classes:

AbstractAuxiliaryContractRule, AbstractBlockContractRule, AbstractLoopContractRule, AbstractLoopInvariantRule, AbstractSideProofRule, AntecTaclet, BlockContractExternalRule, BlockContractInternalRule, CloseAfterMerge, FindTaclet, InfFlowContractAppTaclet, LoopApplyHeadRule, LoopContractExternalRule, LoopContractInternalRule, LoopScopeInvariantRule, MergeRule, ModalitySideProofRule, NoFindTaclet, OneStepSimplifier, QueryExpand, QuerySideProofRule, RewriteTaclet, RuleAppSMT.SMTRule, SuccTaclet, Taclet, UseDependencyContractRule, UseOperationContractRule, WhileInvariantRule

public interface Rule

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.
java.lang.String	displayName() returns the display name of the rule
Name	name() the name of the rule

Method Detail

apply

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

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

Parameters:

goal - the Goal on which to apply ruleApp

services - the Services with the necessary information about the java programs

ruleApp - the rule application to be executed

Returns:

all open goals below \old(goal.node()), i.e. the goals resulting from the rule application

Throws:

java.lang.Exception

RuleAbortException

name

Name name()

the name of the rule

displayName

java.lang.String displayName()

returns the display name of the rule