Sometimes contracts can be specified (and even verified) more easily when they are organized according to different cases of input – and Slang Contracts provides a special notation to support that. Reference intuition for breaking proofs into cases from the math world.

The following example illustrates a variant of the absValue method/contract above that uses Slang’s contract cases::

  def absValueCases(y: Z): Z = {
    Contract(
      Modifies(),
      // case for negative input
      Case("Negative",          // optional string label
           Requires(y < 0),     // condition on input for this case to apply
           Ensures(Res == -y)   // post-condition for this case
      ),
      // case for non-negative input
      Case("Non-negative",      // optional string label
        Requires(y >= 0),       // condition on input for this case to apply
        Ensures(Res == y))      // post-condition for this case
    )

    var ans: Z = 0
    if (x < 0) {
      ans = -y
    } else {
      ans = y
    }
    return ans
  }

There must be a single Modifies clause for contract cases (or the clause can be omitted when no non-local is modified) because Logika does not support a notion of conditional modification (this makes the rest of the verification framework more challenging).

One or more

Case clauses are used, where each Case typically includes both a Requires stating some condition on the input (the case pre-condition) and an Ensures clause indicating the properties (the case post-condition) that must hold in the post-state when the case pre-condition is true.