protected static final class AbstractBlockContractRule.Instantiator extends AbstractAuxiliaryContractRule.Instantiator
Instantiation
s.Constructor and Description |
---|
Instantiator(Term formula,
Goal goal,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
hasApplicableContracts(Services services,
JavaStatement statement,
Modality modality,
Goal goal) |
instantiate
protected boolean hasApplicableContracts(Services services, JavaStatement statement, Modality modality, Goal goal)
hasApplicableContracts
in class AbstractAuxiliaryContractRule.Instantiator
services
- services.statement
- a block or loop.modality
- the current goal's modality.goal
- the current goal.true
iff the block has applicable contracts.