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.0,
Ensures => Sqrt'Result < 10.0);
...
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. Mode Robustness indicates that the precondition and
postcondition of the subprogram should be ignored for this test case.