private static final class BlockContractRule.Instantiator extends Object
Modifier and Type | Field and Description |
---|---|
private Term |
formula |
private Goal |
goal |
private Services |
services |
Constructor and Description |
---|
BlockContractRule.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 StatementBlock |
getFirstBlockInPrefixWithAtLeastOneApplicableContract(Modality modality,
JavaBlock java,
Goal goal) |
private boolean |
hasApplicableContracts(StatementBlock block,
Modality modality,
Goal goal) |
BlockContractRule.Instantiation |
instantiate() |
private final Term formula
private final Goal goal
private final Services services
public BlockContractRule.Instantiation instantiate()
private Term extractUpdate()
private Term extractUpdateTarget()
private Term extractSelf(MethodFrame frame)
private static ExecutionContext extractExecutionContext(MethodFrame frame)
private StatementBlock getFirstBlockInPrefixWithAtLeastOneApplicableContract(Modality modality, JavaBlock java, Goal goal)
private boolean hasApplicableContracts(StatementBlock block, Modality modality, Goal goal)