Re: Run-time checking and speed

[dewar@cs.nyu.edu (Robert Dewar)]

Kent Mitchell asks why one might need to turn off checks in certified code.
Sure the checks will be executed, but presumably you are doing the checks
so that if the check fails, then you do something.

It is the something that is a problem.

Suppose you do constraint error checking in some routine, just to catch
incorrect input from somewhere else in the program, and you have a handler
that defends against bad input.

How will you do coverage testing of the handler, if in fact, as one might
hope, there aren't any bad calls.

Not only compiler generated checks are the issue here. Suppose you write:

   if x > 10 and y > 10 then

	-- Don't know if this can ever happen, but just in case ...

	y := x - 10; -- readjust to acceptable range
   end if;

such code might be appropriate defensive programming in some situations,
but might cause trouble if certification requires coverage testing. There
are three possibilities in a case like this:

  1. You can find a case where the condition is triggered. Fine trigger it
     for the coverage test.

  2. You can prove it never happens. Fine, remove the check

  3. You can't prove it never happens, all your attempts to find the case
     fail, but you can't complete an actual proof.

Case 3 is the tough one, and shows why coverage testing can sometimes
be a double edged sword.

And I have definitely seen situations in which checking has been disabled
precisely because any code conditioned on the checks is impossible or
difficult to coverage testing.

I am not particuarly defending this state of affairs, or the absolute
requirement for coverage testing, just pointing out the situation :-)