Class 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"
         },
        "preSpecifications": [
          {
            "description": "the signalValue must be positive",
            "guard": {
              "conditionText": "signalValue > 0",
              "description": "the signalValue must be positive"
             }
          }
        "postSpecifications": [],
        "throwsSpecifications": [],
        ]
       }
     
    Method SpecificationCollection.getExecutableSpecification(java.lang.reflect.Executable) translates specifications to an ExecutableSpecification object that allows the underlying Boolean expressions to be evaluated.