Class Precondition

A SpecificationClause for pre-conditions on the parameters and receiver of an operation. The pre-condition is expressed as a Guard that is to be checked before the operation is invoked. If the guard evaluates to false on the arguments to the invocation, the operation should not be invoked on the arguments. This means that the sequence with the particular call should be classified as invalid, and discarded.

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

   {
     "description": "the signalValue must be positive",
     "guard": {
        "conditionText": "signalValue > 0",
        "description": "the signalValue must be positive"
      }
   }
 

See Guard for details on specifying guards.