Correction to previous post

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

Someone pointed out to me that an example I previously posted was wrong,
I must have cut-and-pasted the wrong versoin, GRRR!

Here is the example I meant to post:

with Text_IO; use Text_IO;

procedure S is
   Sum : Integer;
begin
   for J in 1 .. 10 loop
      Sum := Sum + J;
   end loop;

   Put_Line (Integer'Image (Sum));
end;

<<the bad one I posted printed out J and was of course illegal>>

And once again, my point was that on some systems, the above program
will give the right result, and therefore pass exhaustive testing,
even though it has a blatant bug. 

The point is that even exhaustive testing is not enough to prove that
a program meets its specifications. Now of course white box testing
using use-def chaining, could with the addition of tools that pointed
out uninitialized paths, find this error, but of course white-box
testing is not an option open to the ACVC testing.

Actually exhuastive coverage and path testing would be a very difficult
task on a program as complex as a compiler for a complex language. The
effort would be huge, and the trouble is that compilers are fluid enough
that the testing would be rapidly out of date, even if you could afford
to do it. I certainly am not aware of any commercial compiler for
Ada, C++, or even C that has been subjected to complete coverage and
path testing (including of course use-def path testing, since that i
is what is involved here).