pragma Test_Case ( [Name =>] static_string_Expression ,[Mode =>] (Nominal | Robustness) [, Requires => Boolean_Expression] [, Ensures => Boolean_Expression]);
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
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
Ensures are valid, where the rules for
Requires are the
same as the rule for an expression in
Precondition and the rules
Ensures are the same as the rule for an expression in
Postcondition. In particular, attributes
'Result can only be used within the
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.
Nominal indicates that the input context should also satisfy the
precondition of the subprogram, and the output context should also satisfy its
Robustness indicates that the precondition and
postcondition of the subprogram should be ignored for this test case.