Class Property


  • public class Property
    extends AbstractBooleanExpression
    The representation of a boolean expression over the values of parameters, receiver object, and return value of a method. The identifiers refer to the values after the method is called. The value of expressions prior to the method call can be referred to by wrapping the expression in "\old(-)". For instance, an expression that states that the method call increases the length of a List object named list by one would be written "list.size() + 1 == \old(list.size())".

    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

       {
          "conditionText": "result >= 0",
          "description": "received value is non-negative"
       }
     

    The identifiers in the guard should be given in the Identifiers for the OperationSpecification containing the SpecificationClause where the property occurs.

    This is identical to Guard, but has a different name to distinguish them in the JSON file.

    • Constructor Detail

      • Property

        public Property​(String description,
                        String conditionText)
        Creates a Property with the given description and condition code.
        Parameters:
        description - the description of this boolean condition
        conditionText - the text of the Java code for the created condition