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

Note

[Robby is “one or more correct”?]

`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.

Note

Address the following: overlapping requires, non-exhaustive requires, ordering of cases (e.g., when overlapping), omitting requires, omitting ensures.