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.
|
ImmutableSet<LoopContract> |
extractLoopContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the loop contracts for the passed labeled statement if it labels
a block.
|
ImmutableSet<LoopContract> |
extractLoopContracts(IProgramMethod method,
LoopStatement loop)
Returns the loop contracts for the passed loop.
|
ImmutableSet<LoopContract> |
extractLoopContracts(IProgramMethod method,
StatementBlock block)
Returns the loop contracts for the passed block.
|
LoopSpecification |
extractLoopInvariant(IProgramMethod pm,
LoopStatement loop)
Returns the loop invariant for the passed loop (if any).
|
ImmutableSet<MergeContract> |
extractMergeContracts(IProgramMethod method,
MergePointStatement mps,
ImmutableList<ProgramVariable> methodParams)
Returns the
MergeContract s for the given
MergePointStatement . |
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
LoopSpecification extractLoopInvariant(IProgramMethod pm, LoopStatement loop) throws SLTranslationException
SLTranslationException
ImmutableSet<BlockContract> extractBlockContracts(IProgramMethod method, StatementBlock block) throws SLTranslationException
method
- the program methodblock
- the statement blockSLTranslationException
ImmutableSet<LoopContract> extractLoopContracts(IProgramMethod method, StatementBlock block) throws SLTranslationException
method
- the program method containing the block.block
- the block.SLTranslationException
- a translation exceptionImmutableSet<LoopContract> extractLoopContracts(IProgramMethod method, LoopStatement loop) throws SLTranslationException
method
- the program method containing the loop.loop
- the loop.SLTranslationException
- a translation exceptionImmutableSet<MergeContract> extractMergeContracts(IProgramMethod method, MergePointStatement mps, ImmutableList<ProgramVariable> methodParams) throws SLTranslationException
MergeContract
s for the given
MergePointStatement
.methodParams
- TODOSLTranslationException
ImmutableSet<BlockContract> extractBlockContracts(IProgramMethod method, LabeledStatement labeled) throws SLTranslationException
method
- the program methodlabeled
- the labeled statementSLTranslationException
- a translation exceptionImmutableSet<LoopContract> extractLoopContracts(IProgramMethod method, LabeledStatement labeled) throws SLTranslationException
method
- the program methodlabeled
- the labeled statementSLTranslationException
- a translation exceptionImmutableSet<PositionedString> getWarnings()