de.uka.ilkd.key.speclang

Interface SpecExtractor

All Known Implementing Classes:

JMLSpecExtractor

public interface SpecExtractor

Extracts specifications from comments.

Method Summary

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 MergeContracts 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.

Method Detail

extractMethodSpecs

ImmutableSet<SpecificationElement> extractMethodSpecs(IProgramMethod pm)
                                               throws SLTranslationException

Returns the operation contracts for the passed operation.

Throws:

SLTranslationException

extractMethodSpecs

ImmutableSet<SpecificationElement> extractMethodSpecs(IProgramMethod pm,
                                                      boolean addInvariant)
                                               throws SLTranslationException

Throws:

SLTranslationException

extractClassSpecs

ImmutableSet<SpecificationElement> extractClassSpecs(KeYJavaType kjt)
                                              throws SLTranslationException

Returns the class invariants for the passed type.

Throws:

SLTranslationException

extractLoopInvariant

LoopSpecification extractLoopInvariant(IProgramMethod pm,
                                       LoopStatement loop)
                                throws SLTranslationException

Returns the loop invariant for the passed loop (if any).

Throws:

SLTranslationException

extractBlockContracts

ImmutableSet<BlockContract> extractBlockContracts(IProgramMethod method,
                                                  StatementBlock block)
                                           throws SLTranslationException

Returns the block contracts for the passed block.

Parameters:

method - the program method

block - the statement block

Returns:

the block contracts

Throws:

SLTranslationException

extractLoopContracts

ImmutableSet<LoopContract> extractLoopContracts(IProgramMethod method,
                                                StatementBlock block)
                                         throws SLTranslationException

Returns the loop contracts for the passed block.

Parameters:

method - the program method containing the block.

block - the block.

Returns:

the loop contracts

Throws:

SLTranslationException - a translation exception

extractLoopContracts

ImmutableSet<LoopContract> extractLoopContracts(IProgramMethod method,
                                                LoopStatement loop)
                                         throws SLTranslationException

Returns the loop contracts for the passed loop.

Parameters:

method - the program method containing the loop.

loop - the loop.

Returns:

the loop contracts

Throws:

SLTranslationException - a translation exception

extractMergeContracts

ImmutableSet<MergeContract> extractMergeContracts(IProgramMethod method,
                                                  MergePointStatement mps,
                                                  ImmutableList<ProgramVariable> methodParams)
                                           throws SLTranslationException

Returns the MergeContracts for the given MergePointStatement.

Parameters:

methodParams - TODO

Throws:

SLTranslationException

extractBlockContracts

ImmutableSet<BlockContract> extractBlockContracts(IProgramMethod method,
                                                  LabeledStatement labeled)
                                           throws SLTranslationException

Returns the block contracts for the passed labeled statement if it labels a block.

Parameters:

method - the program method

labeled - the labeled statement

Returns:

the block contracts

Throws:

SLTranslationException - a translation exception

extractLoopContracts

ImmutableSet<LoopContract> extractLoopContracts(IProgramMethod method,
                                                LabeledStatement labeled)
                                         throws SLTranslationException

Returns the loop contracts for the passed labeled statement if it labels a block.

Parameters:

method - the program method

labeled - the labeled statement

Returns:

the loop contracts

Throws:

SLTranslationException - a translation exception

getWarnings

ImmutableSet<PositionedString> getWarnings()

Returns all warnings generated so far in the translation process. (e.g. this may warn about unsupported features which have been ignored by the translation)