Pragma Test_Case

Syntax:

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

The Test_Case pragma allows defining fine-grain specifications for use by testing tools. The compiler checks the validity of the Test_Case pragma, but its presence does not lead to any modification of the code generated by the compiler.

Test_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 test 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 Test_Case (Name     => "Test 1",
                          Mode     => Nominal,
                          Requires => Arg < 10000,
                          Ensures  => Sqrt'Result < 10);
        ...
     end Math_Functions;

The meaning of a test case is that there is at least one context where Requires holds such that, if the associated subprogram is executed in that context, then Ensures holds 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 test case.