randoop.condition.specification

Class Property

java.lang.Object

randoop.condition.specification.AbstractBooleanExpression

randoop.condition.specification.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 Summary

Constructors

Constructor and Description
Property(java.lang.String description, java.lang.String conditionText) Creates a Property with the given description and condition code.

Method Summary

Methods inherited from class randoop.condition.specification.AbstractBooleanExpression

equals, getConditionSource, getDescription, hashCode, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

Property

public Property(java.lang.String description,
                java.lang.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