public final class LoopContractInternalRule extends AbstractLoopContractRule
Rule for the application of LoopContract
s.
This splits the goal into two branches:
LoopContractInternalBuiltInRuleApp
AbstractLoopContractRule.Instantiator
AbstractAuxiliaryContractRule.Instantiation
Modifier and Type | Field and Description |
---|---|
static LoopContractInternalRule |
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.
|
LoopContractInternalBuiltInRuleApp |
createApp(PosInOccurrence occurrence,
TermServices services) |
Term |
getLastFocusTerm() |
AbstractAuxiliaryContractRule.Instantiation |
getLastInstantiation() |
Name |
name()
the name of the rule
|
protected void |
setLastFocusTerm(Term lastFocusTerm) |
protected void |
setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation) |
contractApplied, createAndRegisterAnonymisationVariables, filterAppliedContracts, getApplicableContracts, getApplicableContracts, instantiate, isApplicable
createLocalAnonUpdate, createLocalVariable, displayName, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getOrigin
public static final LoopContractInternalRule 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 LoopContractInternalBuiltInRuleApp createApp(PosInOccurrence occurrence, TermServices services)
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.