protected abstract static class AbstractAuxiliaryContractRule.Instantiator
extends java.lang.Object
AbstractAuxiliaryContractRule.Instantiation
s.Constructor and Description |
---|
Instantiator(Term formula,
Goal goal,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected abstract boolean |
hasApplicableContracts(Services services,
JavaStatement element,
Modality modality,
Goal goal) |
AbstractAuxiliaryContractRule.Instantiation |
instantiate() |
public AbstractAuxiliaryContractRule.Instantiation instantiate()
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.Copyright © 2003-2019 The KeY-Project.