de.uka.ilkd.key.speclang.jml

Class JMLSpecExtractor

java.lang.Object

de.uka.ilkd.key.speclang.jml.JMLSpecExtractor

All Implemented Interfaces:

SpecExtractor

public final class JMLSpecExtractor
extends java.lang.Object
implements SpecExtractor

Extracts JML class invariants and operation contracts from JML comments. This is the public interface to the jml package. Note that internally, this class is highly similar to the class java.recoderext.JMLTransformer; if you change one of these classes, you probably need to change the other as well.

Field Summary

Fields

Modifier and Type	Field and Description
private static java.lang.String	DEFAULT_SIGNALS_ONLY
private static java.lang.String	ERROR
private JMLSpecFactory	jsf
private static java.lang.String	RUNTIME_EXCEPTION
private Services	services
private static java.lang.String	THROWABLE
private ImmutableSet<PositionedString>	warnings

Constructor Summary

Constructors

Constructor and Description
JMLSpecExtractor(Services services)

Method Summary

Modifier and Type	Method and Description
static int	arrayDepth(Type type, Services services) Get the depth for the nonNull predicate.
private java.lang.String	concatenate(Comment[] comments) Concatenates the passed comments in a position-preserving way.
private ImmutableSet<BlockContract>	createBlockContracts(IProgramMethod method, java.util.List<Label> labels, StatementBlock block, Comment[] comments)
private ImmutableSet<LoopContract>	createLoopContracts(IProgramMethod method, java.util.List<Label> labels, LoopStatement loop, Comment[] comments)
private ImmutableSet<LoopContract>	createLoopContracts(IProgramMethod method, java.util.List<Label> labels, StatementBlock block, Comment[] comments)
static ImmutableSet<PositionedString>	createNonNullPositionedString(java.lang.String varName, KeYJavaType kjt, boolean isImplicitVar, java.lang.String fileName, Position pos, Services services) creates a JML specification expressing that the given variable/field is not null and in case of a reference array type that also its elements are non-null In case of implicit fields or primitive typed fields/variables the empty set is returned
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) Extracts method specifications (i.e., contracts) from Java+JML input.
private java.lang.String	getDefaultSignalsOnly(IProgramMethod pm)
private java.lang.String	getFileName(IProgramMethod method)
private int	getIndexOfMethodDecl(IProgramMethod pm, TextualJMLConstruct[] constructsArray)
ImmutableSet<PositionedString>	getWarnings() Returns all warnings generated so far in the translation process.
private TextualJMLConstruct[]	parseMethodLevelComments(Comment[] comments, java.lang.String fileName)
private Comment[]	removeDuplicates(Comment[] comments)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

THROWABLE

private static final java.lang.String THROWABLE

See Also:

Constant Field Values

ERROR

private static final java.lang.String ERROR

See Also:

Constant Field Values

RUNTIME_EXCEPTION

private static final java.lang.String RUNTIME_EXCEPTION

See Also:

Constant Field Values

DEFAULT_SIGNALS_ONLY

private static final java.lang.String DEFAULT_SIGNALS_ONLY

See Also:

Constant Field Values

services

private final Services services

jsf

private final JMLSpecFactory jsf

warnings

private ImmutableSet<PositionedString> warnings

Constructor Detail

JMLSpecExtractor

public JMLSpecExtractor(Services services)

Method Detail

concatenate

private java.lang.String concatenate(Comment[] comments)

Concatenates the passed comments in a position-preserving way. (see also JMLTransformer::concatenate(), which does the same thing for Recoder ASTs)

getIndexOfMethodDecl

private int getIndexOfMethodDecl(IProgramMethod pm,
                                 TextualJMLConstruct[] constructsArray)

getDefaultSignalsOnly

private java.lang.String getDefaultSignalsOnly(IProgramMethod pm)

createNonNullPositionedString

public static ImmutableSet<PositionedString> createNonNullPositionedString(java.lang.String varName,
                                                                           KeYJavaType kjt,
                                                                           boolean isImplicitVar,
                                                                           java.lang.String fileName,
                                                                           Position pos,
                                                                           Services services)

creates a JML specification expressing that the given variable/field is not null and in case of a reference array type that also its elements are non-null In case of implicit fields or primitive typed fields/variables the empty set is returned

Parameters:

varName - the String specifying the variable/field name

kjt - the KeYJavaType representing the variables/field declared type

isImplicitVar - a boolean indicating if the the field is an implicit one (in which case no

fileName - the String containing the filename where the field/variable has been declared

pos - the Position where to place this implicit specification

Returns:

set of formulas specifying non-nullity for field/variables

arrayDepth

public static int arrayDepth(Type type,
                             Services services)

Get the depth for the nonNull predicate. The depth is 0 for non array types, its dimension for reference array types, and its dimension -1 for array types with primitive base type.

extractClassSpecs

public ImmutableSet<SpecificationElement> extractClassSpecs(KeYJavaType kjt)
                                                     throws SLTranslationException

Description copied from interface: SpecExtractor

Returns the class invariants for the passed type.

Specified by:

extractClassSpecs in interface SpecExtractor

Throws:

SLTranslationException

extractMethodSpecs

public ImmutableSet<SpecificationElement> extractMethodSpecs(IProgramMethod pm)
                                                      throws SLTranslationException

Description copied from interface: SpecExtractor

Returns the operation contracts for the passed operation.

Specified by:

extractMethodSpecs in interface SpecExtractor

Throws:

SLTranslationException

extractMethodSpecs

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

Extracts method specifications (i.e., contracts) from Java+JML input.

Specified by:

extractMethodSpecs in interface SpecExtractor

Parameters:

pm - method to extract for

addInvariant - whether to add static invariants to pre- and post-conditions

Throws:

SLTranslationException

extractBlockContracts

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

Description copied from interface: SpecExtractor

Returns the block contracts for the passed block.

Specified by:

extractBlockContracts in interface SpecExtractor

Parameters:

method - the program method

block - the statement block

Returns:

the block contracts

Throws:

SLTranslationException

extractBlockContracts

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

Description copied from interface: SpecExtractor

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

Specified by:

extractBlockContracts in interface SpecExtractor

Parameters:

method - the program method

labeled - the labeled statement

Returns:

the block contracts

Throws:

SLTranslationException - a translation exception

extractLoopContracts

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

Description copied from interface: SpecExtractor

Returns the loop contracts for the passed loop.

Specified by:

extractLoopContracts in interface SpecExtractor

Parameters:

method - the program method containing the loop.

loop - the loop.

Returns:

the loop contracts

Throws:

SLTranslationException - a translation exception

extractLoopContracts

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

Description copied from interface: SpecExtractor

Returns the loop contracts for the passed block.

Specified by:

extractLoopContracts in interface SpecExtractor

Parameters:

method - the program method containing the block.

block - the block.

Returns:

the loop contracts

Throws:

SLTranslationException - a translation exception

extractLoopContracts

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

Description copied from interface: SpecExtractor

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

Specified by:

extractLoopContracts in interface SpecExtractor

Parameters:

method - the program method

labeled - the labeled statement

Returns:

the loop contracts

Throws:

SLTranslationException - a translation exception

extractMergeContracts

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

Description copied from interface: SpecExtractor

Returns the MergeContracts for the given MergePointStatement.

Specified by:

extractMergeContracts in interface SpecExtractor

methodParams - TODO

Throws:

SLTranslationException

createBlockContracts

private ImmutableSet<BlockContract> createBlockContracts(IProgramMethod method,
                                                         java.util.List<Label> labels,
                                                         StatementBlock block,
                                                         Comment[] comments)
                                                  throws SLTranslationException

Throws:

SLTranslationException

createLoopContracts

private ImmutableSet<LoopContract> createLoopContracts(IProgramMethod method,
                                                       java.util.List<Label> labels,
                                                       LoopStatement loop,
                                                       Comment[] comments)
                                                throws SLTranslationException

Throws:

SLTranslationException

createLoopContracts

private ImmutableSet<LoopContract> createLoopContracts(IProgramMethod method,
                                                       java.util.List<Label> labels,
                                                       StatementBlock block,
                                                       Comment[] comments)
                                                throws SLTranslationException

Throws:

SLTranslationException

getFileName

private java.lang.String getFileName(IProgramMethod method)

parseMethodLevelComments

private TextualJMLConstruct[] parseMethodLevelComments(Comment[] comments,
                                                       java.lang.String fileName)
                                                throws SLTranslationException

Throws:

SLTranslationException

removeDuplicates

private Comment[] removeDuplicates(Comment[] comments)

extractLoopInvariant

public LoopSpecification extractLoopInvariant(IProgramMethod pm,
                                              LoopStatement loop)
                                       throws SLTranslationException

Description copied from interface: SpecExtractor

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

Specified by:

extractLoopInvariant in interface SpecExtractor

Throws:

SLTranslationException

getWarnings

public ImmutableSet<PositionedString> getWarnings()

Description copied from interface: SpecExtractor

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)

Specified by:

getWarnings in interface SpecExtractor