Package randoop.condition.specification

Class Postcondition

java.lang.Object
randoop.condition.specification.SpecificationClause
randoop.condition.specification.Postcondition
public class Postcondition extends SpecificationClause
A Postcondition is a specification clause of a contract on the outcome of the invocation of an operation. The specification consists of a Guard and a Property. For an invocation of the operation, if the Guard evaluates to true, then the Property must also be true.

The JSON serialization of this class is used to read the specifications for an operation given 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 

   {
     "property": {
        "conditionText": "result >= 0",
        "description": "received value is non-negative"
      },
     "description": "returns non-negative received value",
     "guard": {
        "conditionText": "true",
        "description": ""
      }
   }
See the classes Guard and Property for details on specifying those objects.

  • Field Details

    • property

      private final Property property
      The post-condition.

  • Constructor Details

    • Postcondition

      private Postcondition()
      Gson serialization requires a default constructor.

    • Postcondition

      public Postcondition(String description, Guard guard, Property property)
      Creates a Postcondition with the given guard and property.
      Parameters:
      description - the description of the specification
      guard - the Guard for the constructed specification
      property - the Property for the constructed specification

  • Method Details