26.11 Testing with Contracts

gnattest supports pragmas Precondition, Postcondition, and Test_Case. Test routines are generated, one per each Test_Case associated with a tested subprogram. Those test routines have special wrappers for tested functions that have composition of pre- and postcondition of the subprogram with "requires" and "ensures" of the Test_Case (depending on the mode, pre and post either count for Nominal mode or do not count for Robustness mode).

The third example demonstrates how this works:

     cd <install_prefix>/share/examples/gnattest/contracts
     gnattest --harness-dir=driver -Pcontracts.gpr

Putting actual checks within the range of the contract does not cause any error reports. For example, for the test routine which corresponds to test case 1:

     Assert (Sqrt (9.0) = 3.0, "wrong sqrt");

and for the test routine corresponding to test case 2:

     Assert (Sqrt (-5.0) = -1.0, "wrong error indication");

are acceptable:

     cd driver
     gprbuild -Ptest_driver
     test_runner

However, by changing 9.0 to 25.0 and 3.0 to 5.0, for example, you can get a precondition violation for test case one. Also, by using any otherwise correct but positive pair of numbers in the second test routine, you can also get a precondition violation. Postconditions are checked and reported the same way.