Package randoop.condition.specification

Class OperationSpecification

java.lang.Object

randoop.condition.specification.OperationSpecification

public class OperationSpecification
extends Object

A specification of a constructor or method, aka, an operation. Consists of the java.lang.reflect.AccessibleObject for the operation, and lists of Precondition, Postcondition, and ThrowsCondition objects that describe contracts on the operation.

Method SpecificationCollection.create(java.util.List) reads specifications from JSON files. A user specifies JSON files using the --specifications command-line option. The JSON should include a JSON object labeled by the name of each field of this class, as in

 {
   "operation": {
     "classname": "net.Connection",
     "name": "send",
     "parameterTypes": [
       "int"
     ]
   },
   "identifiers": {
     "parameters": [
       "signalValue"
     ],
     "receiverName": "receiver",
     "returnName": "result"
   },
   "pre": [
     {
       "description": "the signalValue must be positive",
       "guard": {
         "conditionText": "signalValue > 0",
         "description": "the signalValue must be positive"
       }
     }
   ],
   "post": [],
   "throws": [],
 }
 

Method SpecificationCollection.getExecutableSpecification(java.lang.reflect.Executable) translates specifications to an ExecutableSpecification object that allows the underlying Boolean expressions to be evaluated.

Field Summary

Fields

Modifier and Type	Field	Description
private Identifiers	identifiers	The identifier names used in the specifications.
private OperationSignature	operation	The reflection object for the operation.
private List<Postcondition>	postSpecifications	The list of post-conditions for the operation.
private List<Precondition>	preSpecifications	The list of pre-conditions for the operation.
private List<ThrowsCondition>	throwsSpecifications	The specification of expected exceptions for the operation.

Constructor Summary

Constructors

Modifier	Constructor	Description
private	OperationSpecification()	Gson serialization requires a default constructor.
	OperationSpecification(OperationSignature operation, Identifiers identifiers)	Creates an OperationSpecification for the given operation with no specifications.
	OperationSpecification(OperationSignature operation, Identifiers identifiers, List<Precondition> preSpecifications, List<Postcondition> postSpecifications, List<ThrowsCondition> throwsSpecifications)	Creates an OperationSpecification for the given operation with the given specifications.

Method Summary

Modifier and Type	Method	Description
void	addParamSpecifications(List<Precondition> specifications)	Adds Precondition objects from the list to this OperationSpecification.
void	addReturnSpecifications(List<Postcondition> specifications)	Adds Postcondition objects from the list to this OperationSpecification.
void	addThrowsConditions(List<ThrowsCondition> specifications)	Adds ThrowsCondition objects from the list to this OperationSpecification.
boolean	equals(Object object)
Identifiers	getIdentifiers()	Return the Identifiers for this specification.
OperationSignature	getOperation()	Return the OperationSignature for the operation.
List<Postcondition>	getPostconditions()	Return the list of Postcondition objects for this OperationSpecification.
List<Precondition>	getPreconditions()	Return the list of Precondition objects for this OperationSpecification.
List<ThrowsCondition>	getThrowsConditions()	Return the list of ThrowsCondition objects for this OperationSpecification.
int	hashCode()
boolean	isEmpty()	Indicates whether this OperationSpecification contains any pre-, post-, or throws-specifications.
String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

operation

private final OperationSignature operation

The reflection object for the operation.

identifiers

private final Identifiers identifiers

The identifier names used in the specifications.

preSpecifications

@SerializedName("pre")
private final List<Precondition> preSpecifications

The list of pre-conditions for the operation.

postSpecifications

@SerializedName("post")
private final List<Postcondition> postSpecifications

The list of post-conditions for the operation.

throwsSpecifications

@SerializedName("throws")
private final List<ThrowsCondition> throwsSpecifications

The specification of expected exceptions for the operation.

Constructor Detail

OperationSpecification

private OperationSpecification()

Gson serialization requires a default constructor.

OperationSpecification

public OperationSpecification(OperationSignature operation,
                              Identifiers identifiers)

Creates an OperationSpecification for the given operation with no specifications.

Parameters:

operation - the OperationSignature object, must be non-null

identifiers - the Identifiers object, must be non-null

OperationSpecification

public OperationSpecification(OperationSignature operation,
                              Identifiers identifiers,
                              List<Precondition> preSpecifications,
                              List<Postcondition> postSpecifications,
                              List<ThrowsCondition> throwsSpecifications)

Creates an OperationSpecification for the given operation with the given specifications.

Parameters:

operation - the reflection object for the operation, must be non-null

identifiers - the identifiers used in the specifications

preSpecifications - the list of param specifications for the operation

postSpecifications - the list of return specifications for the operation

throwsSpecifications - the list of specifications for the operation

Method Detail

getOperation

public OperationSignature getOperation()

Return the OperationSignature for the operation.

Returns:

the reflection object for the operation

getIdentifiers

public Identifiers getIdentifiers()

Return the Identifiers for this specification.

Returns:

the identifiers for this specification

getPreconditions

public List<Precondition> getPreconditions()

Return the list of Precondition objects for this OperationSpecification.

Returns:

the list of Precondition objects for this specification

getPostconditions

public List<Postcondition> getPostconditions()

Return the list of Postcondition objects for this OperationSpecification.

Returns:

the list of Postcondition objects for this specification

getThrowsConditions

public List<ThrowsCondition> getThrowsConditions()

Return the list of ThrowsCondition objects for this OperationSpecification.

Returns:

the list of specifications for this operation specification, is non-null

addParamSpecifications

public void addParamSpecifications(List<Precondition> specifications)

Adds Precondition objects from the list to this OperationSpecification.

Parameters:

specifications - the list of Precondition objects

addReturnSpecifications

public void addReturnSpecifications(List<Postcondition> specifications)

Adds Postcondition objects from the list to this OperationSpecification.

Parameters:

specifications - the list of Postcondition objects

addThrowsConditions

public void addThrowsConditions(List<ThrowsCondition> specifications)

Adds ThrowsCondition objects from the list to this OperationSpecification.

Parameters:

specifications - the list of ThrowsCondition objects

isEmpty

public boolean isEmpty()

Indicates whether this OperationSpecification contains any pre-, post-, or throws-specifications.

Returns:

true if there are no pre-, post-, or throws-specifications, false otherwise

equals

public boolean equals(Object object)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

toString

public String toString()

Overrides:

toString in class Object