Package randoop.condition

Class SpecificationTranslator

java.lang.Object

randoop.condition.SpecificationTranslator

public class SpecificationTranslator
extends Object

Method createExecutableSpecification(java.lang.reflect.Executable, randoop.condition.specification.OperationSpecification, randoop.compile.SequenceCompiler) translates an OperationSpecification object (which has preconditions, postconditions, and throws conditions) to its executable version, ExecutableSpecification.

Field Summary

Fields

Modifier and Type	Field	Description
private SequenceCompiler	compiler	The SequenceCompiler for compiling expression methods.
private static String	DUMMY_VARIABLE_BASE_NAME	The base name of dummy variables used by ObjectContract.
private String	poststateExpressionDeclarations	The parameter declaration string, with parentheses, for a poststate (property) expression method.
private RawSignature	poststateExpressionSignature	The RawSignature for a poststate (property) expression method.
private String	prestateExpressionDeclaration	The parameter part of a method declaration string, with parentheses, for a prestate (guard) expression method.
private RawSignature	prestateExpressionSignature	The RawSignature for a prestate (guard) expression method.
private Map<String,String>	replacementMap	The map of expression identifiers to dummy variables.

Constructor Summary

Constructors

Modifier	Constructor	Description
private	SpecificationTranslator(RawSignature prestateExpressionSignature, String prestateExpressionDeclaration, RawSignature poststateExpressionSignature, String poststateExpressionDeclaration, Map<String,String> replacementMap, SequenceCompiler compiler)	Creates a SpecificationTranslator object in the given package with the signature strings and variable replacementMap.

Method Summary

Modifier and Type	Method	Description
private ExecutableBooleanExpression	create(Guard expression)	Creates a ExecutableBooleanExpression object for the given AbstractBooleanExpression using the prestate expression signature of this SpecificationTranslator.
ExecutableBooleanExpression	create(Property expression)	Creates a ExecutableBooleanExpression object for the given AbstractBooleanExpression using the poststate expression signature of this SpecificationTranslator.
static ExecutableSpecification	createExecutableSpecification(Executable executable, OperationSpecification specification, SequenceCompiler compiler)	Create the ExecutableSpecification object for the given OperationSpecification using this SpecificationTranslator.
private static Map<String,String>	createReplacementMap(List<String> parameterNames)	Creates the replacement map from the given parameter names to numbered dummy variable names as used in ObjectContract.
(package private) static SpecificationTranslator	createTranslator(Executable executable, OperationSpecification specification, SequenceCompiler compiler)	Creates a SpecificationTranslator object to translate the OperationSpecification of executable.
(package private) SequenceCompiler	getCompiler()	Returns the compiler from this object.
private static RawSignature	getExpressionSignature(Executable executable, boolean postState)	Create the RawSignature for evaluating an expression about a method call to the given method or constructor.
private List<ExecutableBooleanExpression>	getGuardExpressions(List<Precondition> preconditions)	Construct the list of ExecutableBooleanExpression objects, one for each Precondition.
(package private) String	getPoststateExpressionDeclarations()	Return the poststate expression method parameter declaration string.
(package private) RawSignature	getPoststateExpressionSignature()	Returns the poststate expression method signature from this object.
(package private) String	getPrestateExpressionDeclaration()	Return the prestate expression method parameter declaration string.
private static RawSignature	getRawSignature(@DotSeparatedIdentifiers String packageName, @Nullable Class<?> receiverAType, Class<?>[] parameterTypes, Class<?> returnType)	Creates a RawSignature for an expression method.
(package private) Map<String,String>	getReplacementMap()	Returns the replacement map for the identifiers in the expression to the dummy variables expected in contract assertions.
private List<GuardPropertyPair>	getReturnConditions(List<Postcondition> postconditions)	Construct the list of GuardPropertyPair objects, one for each Postcondition in postconditions.
private List<GuardThrowsPair>	getThrowsConditions(List<ThrowsCondition> throwsConditions)	Construct the list of GuardThrowsPair objects, one for each ThrowsCondition in throwsConditions.
private static @DotSeparatedIdentifiers String	renamedPackage(Package aPackage)	Gets the name of the package.

Methods inherited from class java.lang.Object

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

Field Detail

DUMMY_VARIABLE_BASE_NAME

private static final String DUMMY_VARIABLE_BASE_NAME

The base name of dummy variables used by ObjectContract.

See Also:

Constant Field Values

prestateExpressionSignature

private RawSignature prestateExpressionSignature

The RawSignature for a prestate (guard) expression method.

prestateExpressionDeclaration

private final String prestateExpressionDeclaration

The parameter part of a method declaration string, with parentheses, for a prestate (guard) expression method.

poststateExpressionSignature

private RawSignature poststateExpressionSignature

The RawSignature for a poststate (property) expression method.

poststateExpressionDeclarations

private final String poststateExpressionDeclarations

The parameter declaration string, with parentheses, for a poststate (property) expression method.

replacementMap

private final Map<String,String> replacementMap

The map of expression identifiers to dummy variables.

compiler

private final SequenceCompiler compiler

The SequenceCompiler for compiling expression methods.

Constructor Detail

SpecificationTranslator

private SpecificationTranslator(RawSignature prestateExpressionSignature,
                                String prestateExpressionDeclaration,
                                RawSignature poststateExpressionSignature,
                                String poststateExpressionDeclaration,
                                Map<String,String> replacementMap,
                                SequenceCompiler compiler)

Creates a SpecificationTranslator object in the given package with the signature strings and variable replacementMap.

Parameters:

prestateExpressionSignature - the RawSignature for a prestate expression method

prestateExpressionDeclaration - the parameter declaration string, with parentheses, for a prestate expression method

poststateExpressionSignature - the RawSignature for a poststate expression method

poststateExpressionDeclaration - the parameter declaration string, with parentheses, for a poststate expression method

replacementMap - the map of expression identifiers to dummy variables

compiler - the SequenceCompiler for creating expression methods

Method Detail

createTranslator

static SpecificationTranslator createTranslator(Executable executable,
                                                OperationSpecification specification,
                                                SequenceCompiler compiler)

Creates a SpecificationTranslator object to translate the OperationSpecification of executable.

Parameters:

executable - the java.lang.reflect.AccessibleObject for the operation with OperationSpecification to translate

specification - the specification to be translated

compiler - the sequence compiler to use to create expression methods

Returns:

the translator object to convert the specifications for executable

getExpressionSignature

private static RawSignature getExpressionSignature(Executable executable,
                                                   boolean postState)

Create the RawSignature for evaluating an expression about a method call to the given method or constructor.

The parameter types of the RawSignature are the declaring class as the receiver type, followed by the parameter types of executable, followed by the return type if postState is true and executable is not a void method. These are all needed, in case the expression refers to them.

Note: The declaring class of the expression method is actually determined by ExecutableBooleanExpression.createMethod(RawSignature, String, String, SequenceCompiler).

Parameters:

executable - the method or constructor to which the expression belongs

postState - if true, include a variable for the return value in the signature

Returns:

the RawSignature for a expression method of executable

getRawSignature

private static RawSignature getRawSignature(@DotSeparatedIdentifiers String packageName,
                                            @Nullable Class<?> receiverAType,
                                            Class<?>[] parameterTypes,
                                            Class<?> returnType)

Creates a RawSignature for an expression method.

Note that these signatures may be used more than once for different expression methods, and so ExecutableBooleanExpression.createMethod(RawSignature, String, String, SequenceCompiler) replaces the classname to ensure a unique name.

Parameters:

packageName - the package name for the expression class, or null for the default package

receiverAType - the declaring class of the method or constructor, included first in parameter types if non-null

parameterTypes - the parameter types for the original method or constructor

returnType - the return type for the method, or the declaring class for a constructor, included last in parameter types if non-null

Returns:

the constructed post-expression method signature

renamedPackage

private static @DotSeparatedIdentifiers String renamedPackage(Package aPackage)

Gets the name of the package. If the package name begins with "java.", prefixes it by "randoop.", since user classes cannot be added to the java package.

Parameters:

aPackage - the package to get the name of, may be null

Returns:

the name of the package, updated to start with "randoop." if the original begins with "java."; null if aPackage is null

createReplacementMap

private static Map<String,String> createReplacementMap(List<String> parameterNames)

Creates the replacement map from the given parameter names to numbered dummy variable names as used in ObjectContract.

Parameters:

parameterNames - the parameter names of the expression methods

Returns:

the map from the parameter names to dummy variables

createExecutableSpecification

public static ExecutableSpecification createExecutableSpecification(Executable executable,
                                                                    OperationSpecification specification,
                                                                    SequenceCompiler compiler)

Create the ExecutableSpecification object for the given OperationSpecification using this SpecificationTranslator.

Parameters:

executable - the java.lang.reflect.AccessibleObject for the operation to translate

specification - the specification to translate

compiler - the sequence compiler to use to create expression methods

Returns:

the ExecutableSpecification for the given specification

getGuardExpressions

private List<ExecutableBooleanExpression> getGuardExpressions(List<Precondition> preconditions)

Construct the list of ExecutableBooleanExpression objects, one for each Precondition.

Parameters:

preconditions - the list of Precondition objects that will be converted to ExecutableBooleanExpression

Returns:

the list of ExecutableBooleanExpression objects obtained by converting each Precondition

getReturnConditions

private List<GuardPropertyPair> getReturnConditions(List<Postcondition> postconditions)

Construct the list of GuardPropertyPair objects, one for each Postcondition in postconditions.

Parameters:

postconditions - the list of Postcondition that will be converted to GuardPropertyPair objects

Returns:

the list of GuardPropertyPair objects obtained by converting each Postcondition

getThrowsConditions

private List<GuardThrowsPair> getThrowsConditions(List<ThrowsCondition> throwsConditions)

Construct the list of GuardThrowsPair objects, one for each ThrowsCondition in throwsConditions.

Parameters:

throwsConditions - the list of ThrowsCondition that will be converted to GuardPropertyPair objects

Returns:

the list of GuardPropertyPair objects obtained by converting each ThrowsCondition

create

private ExecutableBooleanExpression create(Guard expression)

Creates a ExecutableBooleanExpression object for the given AbstractBooleanExpression using the prestate expression signature of this SpecificationTranslator.

Parameters:

expression - the AbstractBooleanExpression to be converted

Returns:

the ExecutableBooleanExpression object for expression

create

public ExecutableBooleanExpression create(Property expression)

Creates a ExecutableBooleanExpression object for the given AbstractBooleanExpression using the poststate expression signature of this SpecificationTranslator.

Parameters:

expression - the AbstractBooleanExpression to be converted

Returns:

the ExecutableBooleanExpression object for expression

getPrestateExpressionDeclaration

String getPrestateExpressionDeclaration()

Return the prestate expression method parameter declaration string. Includes parentheses.

Only used for testing.

Returns:

the prestate expression method parameter declaration string

getPoststateExpressionDeclarations

String getPoststateExpressionDeclarations()

Return the poststate expression method parameter declaration string. Includes parentheses.

Only used for testing.

Returns:

the poststate expression method parameter declaration string

getPoststateExpressionSignature

RawSignature getPoststateExpressionSignature()

Returns the poststate expression method signature from this object. This signature includes the parameters of the prestate expression signature, plus the return type.

Only used for testing.

Returns:

the poststate expression method signature for this object

getCompiler

SequenceCompiler getCompiler()

Returns the compiler from this object.

Only used for testing. ||||||| merged common ancestors

Only used for testing.

Returns:

the compiler for this object

getReplacementMap

Map<String,String> getReplacementMap()

Returns the replacement map for the identifiers in the expression to the dummy variables expected in contract assertions.

Returns:

the replacement map for the identifiers in the expression