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 and verification tools. The compiler checks its validity but the presence of pragma Test_Case 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 < 100,
                          Ensures  => Sqrt'Result < 10);
        ...
     end Math_Functions;

The meaning of a test case is that, if 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 satisfy the precondition of the subprogram, and the output context should then satisfy its postcondition. More Robustness indicates that the pre- and postcondition of the subprogram should be ignored for this test case.