Pragma Test_Case (GNAT Reference Manual)

### 2.186 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.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.