public final class LoopContractExternalRule extends AbstractLoopContractRule
Rule for the application of LoopContract
s.
This splits the goal into two branches:
The validity of all LoopContract
s that were used in the application of this rule must be
proven in a FunctionalLoopContractPO
before the current proof is considered closed.
LoopContractExternalBuiltInRuleApp
AbstractLoopContractRule.Instantiator
AbstractAuxiliaryContractRule.Instantiation
Modifier and Type | Field and Description |
---|---|
static LoopContractExternalRule |
INSTANCE
The only instance of this class.
|
FULL_PRECONDITION_TERM_HINT, NEW_POSTCONDITION_TERM_HINT
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.
|
IBuiltInRuleApp |
createApp(PosInOccurrence pos,
TermServices services) |
Term |
getLastFocusTerm() |
AbstractAuxiliaryContractRule.Instantiation |
getLastInstantiation() |
boolean |
isApplicable(Goal goal,
PosInOccurrence occurrence)
returns true iff a rule is applicable at the given
position.
|
Name |
name()
the name of the rule
|
protected void |
setLastFocusTerm(Term lastFocusTerm) |
protected void |
setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation) |
contractApplied, createAndRegisterAnonymisationVariables, filterAppliedContracts, getApplicableContracts, getApplicableContracts, instantiate
createLocalAnonUpdate, createLocalVariable, displayName, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getOrigin
public static final LoopContractExternalRule INSTANCE
public Term getLastFocusTerm()
getLastFocusTerm
in class AbstractAuxiliaryContractRule
protected void setLastFocusTerm(Term lastFocusTerm)
setLastFocusTerm
in class AbstractAuxiliaryContractRule
lastFocusTerm
- the last focus term.AbstractAuxiliaryContractRule.getLastFocusTerm()
public AbstractAuxiliaryContractRule.Instantiation getLastInstantiation()
getLastInstantiation
in class AbstractAuxiliaryContractRule
protected void setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation)
setLastInstantiation
in class AbstractAuxiliaryContractRule
lastInstantiation
- the last instantiation.AbstractAuxiliaryContractRule.getLastInstantiation()
public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services)
public boolean isApplicable(Goal goal, PosInOccurrence occurrence)
BuiltInRule
isApplicable
in interface BuiltInRule
isApplicable
in class AbstractLoopContractRule
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp) throws RuleAbortException
Rule
goal
- the Goal on which to apply ruleAppservices
- the Services with the necessary information
about the java programsruleApp
- the rule application to be executedRuleAbortException
Copyright © 2003-2019 The KeY-Project.