Pragma Contract_Case

Syntax:

     pragma Contract_Case (
        [Name     =>] static_string_Expression
       ,[Mode     =>] (Nominal | Robustness)
      [, Requires =>  Boolean_Expression]
      [, Ensures  =>  Boolean_Expression]);

The Contract_Case pragma allows defining fine-grain specifications that can complement or replace the contract given by a precondition and a postcondition. Additionally, the Contract_Case 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 case

     pragma Contract_Case (
        Name     => ...
        Mode     => ...
        Requires => R,
        Ensures  => E);

is equivalent to

     pragma Postcondition (not R'Old or else E);

which is also equivalent to (in Ada 2012)

     pragma Postcondition (if R'Old then E);

expressing that, whenever condition R is satisfied on entry to the subprogram, condition E should be fulfilled on exit to the subprogram.

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

     pragma Contract_Case (
        Name     => "Replace precondition",
        Mode     => Nominal,
        Requires => not P,
        Ensures  => False);
     pragma Contract_Case (
        Name     => "Replace postcondition",
        Mode     => Nominal,
        Requires => P,
        Ensures  => Q);

Contract_Case pragmas may only appear immediately following the (separate) declaration of a subprogram in a package declaration, inside a package spec unit. Only other pragmas may intervene (that is appear between the subprogram declaration and a contract case).

The compiler checks that boolean expressions given in Requires and Ensures are valid, where the rules for Requires are the same as the rule for an expression in Precondition and the rules for Ensures are the same as the rule for an expression in Postcondition. In particular, attributes 'Old and 'Result can only be used within the Ensures expression. The following is an example of use within a package spec:

     package Math_Functions is
        ...
        function Sqrt (Arg : Float) return Float;
        pragma Contract_Case (Name     => "Small argument",
                              Mode     => Nominal,
                              Requires => Arg < 100,
                              Ensures  => Sqrt'Result < 10);
        ...
     end Math_Functions;

The meaning of a contract case is that, whenever the associated subprogram is executed in a context where Requires holds, then Ensures should hold when the subprogram returns. Mode Nominal indicates that the input context should also satisfy the precondition of the subprogram, and the output context should also satisfy its postcondition. More Robustness indicates that the precondition and postcondition of the subprogram should be ignored for this contract case, which is mostly useful when testing such a contract using a testing tool that understands contract cases.