Re: Ada Core Technologies and Ada95 Standards

[eachus@spectre.mitre.org (Robert I. Eachus)]

In article <4kf739$f00@cliffy.lfwc.lockheed.com> l117593@cliffy.lfwc.lockheed.com (Cordes MJ) writes:

  > I don't think that Ken, or anybody else in the user community,
  > expects the ACVC to guarantee 100% compliance with the RM. I did,
  > however, believe that the ACVC provided *some* measure of
  > quality. You two can concentrate on the pathological cases and
  > make a strong argument for doing nothing while we continue to
  > develop safety critical code with *validated* compilers which
  > generate bad code for some of the more simple Ada features.

    Very much the wrong conclusion to draw from our posts.  Robert
Dewar and I have been involved for over fifteen years with many other
experts representing both the user community and the compiler
developers in making Ada compilers the highest quality compilers
available for any language.  None of the ARG members, the AVO testers,
the ACVC developers or even the commpiler developers has ever had any
goal for the ACVC suite other than for it to be the best test suite
possible for validating compilers.  On several occaisions, I have run
into a bug in the compiler I'm developing, created a test and
forwarded it to the AVO because I thought the ACVC suite should have
caught the bug. (Of course the test also ended up in my regression
suite.) I'm sure Robert Dewar had done the same thing--in addition to
creating a whole suite of chapter 13 tests.

   Now having said that, back to the flip side of the issue.  There
are a number of profoundly disturbing results in computability theory,
among them Post's Correspondence Problem and Godel's Proof.  (Go read
Godel, Escher, Bach if you are not familiar with these issues.)  Most
computer programs never bump into these limits, by compilers by their
nature start out there.  It is trivially easy to prove that set of
programs accepted by your Ada compiler can never be proven to be the
same set of programs accepted by my compiler.  (In fact as you will
see, it is quite easy to prove that the sets are different.)  The same
issue prevents your, say, C compiler vendor from proving that his C
compiler accepts all legal C programs, and reject all programs that
are not legal C.

   It gets worse.  Ada is a complex enough language, in the sense of
Godel's proof, that I can demonstrate that ANY Ada compiler either
accepts illegal programs or rejects legal Ada programs.  Compiler
vendors hope that this limit on the perfectability of compilers can be
pushed into the realm of capacity limits.  In other words, that the
incorrectly rejected programs are so large that any attempt to
compiler them runs into memory limits.  But Godel's proof, in spite of
being a constructive proof, fails to provide such a lower limit.  We
do the best we can, test the hell out of the compilers, and keep a
weather eye open.

    Now you know why I switched to C in the paragraph above.  In Ada
there are some cases where the legality of programs depends on whether
or not an exception will be raised by the evaluation of some otherwise
static expression at run time, and it is perfectly legal Ada to put a
Godelian embedding into such expressions.

   It seems farfetched, but I once demonstrated a case where one
compiler accepted a program as legal Ada 83 and another compiler
rejected it as illegal, and BOTH were right...The program was illegal
if, and only if, it raised Constraint_Error when run, and the
expression that could raise Constraint_Error was one where 11.6 allows
the compiler to use a wider range to evaluate it.  So there you have
it, a very unpathological seeming program, and it is undecidable
whether or not it was legal Ada.  I won't include the entire program,
but the key lines are:

   type Int_16 is range -2**15..2**15-1;
   subtype Positive_16 is Int_16 range 1..2**15-1;
   P: Positive_16 := 10;
   ...
   case P is
     when 1..10 => ...
     when 11..Positive_16'LAST => ...
     -- no others clause here...
   end case;

   I'm sure you will all be happy to know that this case was fixed by
the preference rule in Ada 95.  My example program is always legal Ada
95, but I am sure that there are others.  Godel tells me so.  (In fact
I think I can modify this example to avoid the preference rule, but
I'll wait.)

   For those of you trying to puzzle the example out, a few hints.
Case statements require an others clause if the subtype of the
expression is non-static.  Positive_16 is a static subtype if its
bounds are static.  The upper bound is an expression of type Int_16,
and evaluating 2**15 may or may not raise an exception if evaluated at
run-time.  It doesn't matter when it IS evaluated, just whether or not
it would raise an exception, if evaluated at run-time.  The compiler
decides this, then marks Positive_16 as static or non-static.
Incidently, the first 2**16 is not of type Int_16, and is not allowed
to raise an exception.
--

					Robert I. Eachus

with Standard_Disclaimer;
use  Standard_Disclaimer;
function Message (Text: in Clever_Ideas) return Better_Ideas is...