Pragma Contract_Cases

Syntax:

     pragma Contract_Cases (
        Condition => Consequence
      {,Condition => Consequence});

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 conditions is satisfied on entry to the subprogram. The postcondition ensures that for the condition that was True on entry, the corrresponding 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 conditions and consequences are valid, where the rules for conditions 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 condition 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 .. 99) => Sqrt'Result < 10,
                               Arg >= 100       => Sqrt'Result >= 10,
                               others           => Sqrt'Result = 0);
        ...
     end Math_Functions;

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