public interface POExtension
ProofOblInput
.
Implementations are instantiated once via ProofInitServiceUtil#createOperationPOExtension(ProofOblInput)
and reused all the time. This means that POExtension
are singletons and should not have a state.
Modifier and Type | Method and Description |
---|---|
boolean |
isPOSupported(ProofOblInput po)
Checks if the given
ProofOblInput is supported. |
Term |
modifyPostTerm(InitConfig proofConfig,
Services services,
Term postTerm)
Modifies the post condition.
|
boolean isPOSupported(ProofOblInput po)
ProofOblInput
is supported.po
- The ProofOblInput
to check.true
is supported, false
is not supported.Term modifyPostTerm(InitConfig proofConfig, Services services, Term postTerm)
proofConfig
- The InitConfig
to use.services
- The Services
to use.postTerm
- The post condition to modify.