Pragma Contract_Cases (GNAT Reference Manual)

### 2.36 Pragma Contract_Cases ¶

Syntax:

    pragma Contract_Cases (CONTRACT_CASE {, CONTRACT_CASE});

    CONTRACT_CASE ::= CASE_GUARD => CONSEQUENCE

    CASE_GUARD ::= boolean_EXPRESSION | others

    CONSEQUENCE ::= boolean_EXPRESSION

The `Contract_Cases` pragma allows defining fine-grain specifications that can complement or replace the contract given by a precondition and a postcondition. Additionally, the `Contract_Cases` pragma can be used by testing and formal verification tools. The compiler checks its validity and, depending on the assertion policy at the point of declaration of the pragma, it may insert a check in the executable. For code generation, the contract cases

    pragma Contract_Cases (
      Cond1 => Pred1,
      Cond2 => Pred2);

are equivalent to

    C1 : constant Boolean := Cond1;  --  evaluated at subprogram entry
    C2 : constant Boolean := Cond2;  --  evaluated at subprogram entry
    pragma Precondition ((C1 and not C2) or (C2 and not C1));
    pragma Postcondition (if C1 then Pred1);
    pragma Postcondition (if C2 then Pred2);

The precondition ensures that one and only one of the case guards is satisfied on entry to the subprogram. The postcondition ensures that for the case guard that was True on entry, the corresponding consequence is True on exit. Other consequence expressions are not evaluated.

A precondition `P` and postcondition `Q` can also be expressed as contract cases:

    pragma Contract_Cases (P => Q);

The placement and visibility rules for `Contract_Cases` pragmas are identical to those described for preconditions and postconditions.

The compiler checks that boolean expressions given in case guards and consequences are valid, where the rules for case guards are the same as the rule for an expression in `Precondition` and the rules for consequences are the same as the rule for an expression in `Postcondition`. In particular, attributes `'Old` and `'Result` can only be used within consequence expressions. The case guard for the last contract case may be `others`, to denote any case not captured by the previous cases. The following is an example of use within a package spec:

    package Math_Functions is
       ...
       function Sqrt (Arg : Float) return Float;
       pragma Contract_Cases (((Arg in 0.0 .. 99.0) => Sqrt'Result < 10.0,
                               Arg >= 100.0         => Sqrt'Result >= 10.0,
                               others               => Sqrt'Result = 0.0));
       ...
    end Math_Functions;

The meaning of contract cases is that only one case should apply at each call, as determined by the corresponding case guard evaluating to True, and that the consequence for this case should hold when the subprogram returns.

This is an assertion kind pragma that can associate a set of its arguments with an assertion level. See SPARK 2014 Reference Manual, section 11.4.2.