protected abstract static class AbstractAuxiliaryContractRule.Instantiator
extends java.lang.Object
AbstractAuxiliaryContractRule.Instantiation
s.Modifier and Type | Field and Description |
---|---|
private Term |
formula
The formula on which the rule is to be applied.
|
private Goal |
goal
The current goal.
|
private Services |
services
Services.
|
Constructor and Description |
---|
Instantiator(Term formula,
Goal goal,
Services services) |
Modifier and Type | Method and Description |
---|---|
private static ExecutionContext |
extractExecutionContext(MethodFrame frame) |
private Term |
extractSelf(MethodFrame frame) |
private Term |
extractUpdate() |
private Term |
extractUpdateTarget() |
private JavaStatement |
getFirstStatementInPrefixWithAtLeastOneApplicableContract(Modality modality,
JavaBlock java,
Goal goal) |
protected abstract boolean |
hasApplicableContracts(Services services,
JavaStatement element,
Modality modality,
Goal goal) |
AbstractAuxiliaryContractRule.Instantiation |
instantiate() |
private final Term formula
private final Goal goal
private final Services services
public AbstractAuxiliaryContractRule.Instantiation instantiate()
private Term extractUpdate()
formula
is an update application, null
otherwise.private Term extractUpdateTarget()
formula
is an update application, formula
otherwise.private Term extractSelf(MethodFrame frame)
frame
- the outermost method-frame used in the formula.private static ExecutionContext extractExecutionContext(MethodFrame frame)
frame
- the outermost method-frame used in the formula.private JavaStatement getFirstStatementInPrefixWithAtLeastOneApplicableContract(Modality modality, JavaBlock java, Goal goal)
modality
- the contract's modality.java
- the java block.goal
- the current goal.protected abstract boolean hasApplicableContracts(Services services, JavaStatement element, Modality modality, Goal goal)
services
- services.element
- a block or loop.modality
- the current goal's modality.goal
- the current goal.true
iff the block has applicable contracts.