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