public interface SpecExtractor
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
extractBlockContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the block contracts for the passed labeled statement if it labels a block.
|
ImmutableSet<BlockContract> |
extractBlockContracts(IProgramMethod method,
StatementBlock block)
Returns the block contracts for the passed block.
|
ImmutableSet<SpecificationElement> |
extractClassSpecs(KeYJavaType kjt)
Returns the class invariants for the passed type.
|
LoopInvariant |
extractLoopInvariant(IProgramMethod pm,
LoopStatement loop)
Returns the loop invariant for the passed loop (if any).
|
ImmutableSet<SpecificationElement> |
extractMethodSpecs(IProgramMethod pm)
Returns the operation contracts for the passed operation.
|
ImmutableSet<SpecificationElement> |
extractMethodSpecs(IProgramMethod pm,
boolean addInvariant) |
ImmutableSet<PositionedString> |
getWarnings()
Returns all warnings generated so far in the translation process.
|
ImmutableSet<SpecificationElement> extractMethodSpecs(IProgramMethod pm) throws SLTranslationException
SLTranslationException
ImmutableSet<SpecificationElement> extractMethodSpecs(IProgramMethod pm, boolean addInvariant) throws SLTranslationException
SLTranslationException
ImmutableSet<SpecificationElement> extractClassSpecs(KeYJavaType kjt) throws SLTranslationException
SLTranslationException
LoopInvariant extractLoopInvariant(IProgramMethod pm, LoopStatement loop) throws SLTranslationException
SLTranslationException
ImmutableSet<BlockContract> extractBlockContracts(IProgramMethod method, StatementBlock block) throws SLTranslationException
SLTranslationException
ImmutableSet<BlockContract> extractBlockContracts(IProgramMethod method, LabeledStatement labeled) throws SLTranslationException
SLTranslationException
ImmutableSet<PositionedString> getWarnings()