de.uka.ilkd.key.rule

Interface BuiltInRule

All Superinterfaces:

Rule

All Known Implementing Classes:

AbstractAuxiliaryContractRule, AbstractBlockContractRule, AbstractLoopContractRule, AbstractLoopInvariantRule, AbstractSideProofRule, BlockContractExternalRule, BlockContractInternalRule, CloseAfterMerge, LoopApplyHeadRule, LoopContractExternalRule, LoopContractInternalRule, LoopScopeInvariantRule, MergeRule, ModalitySideProofRule, OneStepSimplifier, QueryExpand, QuerySideProofRule, RuleAppSMT.SMTRule, UseDependencyContractRule, UseOperationContractRule, WhileInvariantRule

public interface BuiltInRule
extends Rule

Buit-in rule interface. As applications of this rule kind may not be successful in each case one has to ensure that the goal split is done only iff the application was successful.

Method Summary

Modifier and Type	Method and Description
IBuiltInRuleApp	createApp(PosInOccurrence pos, TermServices services)
boolean	isApplicable(Goal goal, PosInOccurrence pio) returns true iff a rule is applicable at the given position.
boolean	isApplicableOnSubTerms()

Methods inherited from interface de.uka.ilkd.key.rule.Rule

apply, displayName, name

Method Detail

isApplicable

boolean isApplicable(Goal goal,
                     PosInOccurrence pio)

returns true iff a rule is applicable at the given position. This does not necessarily mean that a rule application will change the goal (this decision is made due to performance reasons)

isApplicableOnSubTerms

boolean isApplicableOnSubTerms()

createApp

IBuiltInRuleApp createApp(PosInOccurrence pos,
                          TermServices services)