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 Details

    • 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 Details

    • 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 Details