public final class BlockContractInternalRule extends AbstractBlockContractRule
Rule for the application of BlockContract
s.
This splits the goal into two branches:
BlockContractInternalBuiltInRuleApp
AbstractBlockContractRule.BlockContractHint, AbstractBlockContractRule.InfFlowValidityData, AbstractBlockContractRule.Instantiator
AbstractAuxiliaryContractRule.Instantiation
Modifier and Type | Field and Description |
---|---|
static BlockContractInternalRule |
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.
|
BlockContractInternalBuiltInRuleApp |
createApp(PosInOccurrence occurrence,
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) |
buildAfterVar, buildInfFlowPostAssumption, buildInfFlowPreAssumption, buildLocalOutsAtPost, buildLocalOutsAtPre, contractApplied, createAndRegisterAnonymisationVariables, filterAppliedContracts, getApplicableContracts, getApplicableContracts, instantiate, setUpInfFlowPartOfUsageGoal, setUpInfFlowValidityGoal
createLocalAnonUpdate, createLocalVariable, displayName, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getOrigin
public static final BlockContractInternalRule 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 BlockContractInternalBuiltInRuleApp 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
public boolean isApplicable(Goal goal, PosInOccurrence occurrence)
BuiltInRule
isApplicable
in interface BuiltInRule
isApplicable
in class AbstractBlockContractRule
Copyright © 2003-2019 The KeY-Project.