Class Guard


public class Guard extends AbstractBooleanExpression
The representation of a boolean expression over the values of parameters and receiver object of an operation (i.e., a method or constructor). The identifiers refer to the values before the operation is called.

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": "signalValue > 0",
      "description": "the signal value must be positive"
   }
 

where signalValue is a declared identifier in the specification.

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

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

See Also:
  • Constructor Details

    • Guard

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