From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,42427d0d1bf647b1 X-Google-Attributes: gid103376,public From: eachus@spectre.mitre.org (Robert I. Eachus) Subject: Re: Ada Core Technologies and Ada95 Standards Date: 1996/04/11 Message-ID: X-Deja-AN: 146989584 references: <00001a73+00002c20@msn.com> organization: The Mitre Corp., Bedford, MA. newsgroups: comp.lang.ada Date: 1996-04-11T00:00:00+00:00 List-Id: 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...