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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII X-Google-Thread: 103376,a00006d3c4735d70 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2004-01-16 21:19:18 PST Path: archiver1.google.com!news2.google.com!newsfeed2.dallas1.level3.net!news.level3.com!zeus.visi.com!news-out.visi.com!green.octanews.net!news.octanews.net!news-xfer.cox.net!peer02.cox.net!cox.net!pd7cy1no!shaw.ca!border1.nntp.ash.giganews.com!border2.nntp.sjc.giganews.com!border1.nntp.sjc.giganews.com!nntp.giganews.com!local1.nntp.sjc.giganews.com!nntp.comcast.com!news.comcast.com.POSTED!not-for-mail NNTP-Posting-Date: Fri, 16 Jan 2004 23:19:16 -0600 Date: Sat, 17 Jan 2004 00:19:15 -0500 From: "Robert I. Eachus" User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.4) Gecko/20030624 Netscape/7.1 (ax) X-Accept-Language: en-us, en MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems References: <0F6Nb.1623$Tt.642@reader1.news.jippii.net> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit Message-ID: NNTP-Posting-Host: 24.34.214.193 X-Trace: sv3-EeXD5lTZSE+9CcUORzjPteO8KVdB3R1lP1lMuqctV+t7XGXv2jrSbT0TA+C92kAWzyj65mLV9D5oz43!ZvB0+4rz2y6G5NCPj4+ottXUntFx+YCHFFVsmwmlMbC0yPsWaE69CgZipJF8aw== X-Complaints-To: abuse@comcast.net X-DMCA-Complaints-To: dmca@comcast.net X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.1 Xref: archiver1.google.com comp.lang.ada:4481 Date: 2004-01-17T00:19:15-05:00 List-Id: Aatu Koskensilta wrote: > (#) Surely this is not the case for arbitrary formulae? If it is, Ada > seems rather an odd language; I've never encountered an actually used > computer language with correctness of a program not arithmetic. As far as this particular case is concerned. Yes, that is what I am saying. Actually, back when MIL-STD 1815 was Ada and the ANSI standard effort was in progress, I wrote an example program that was legal Ada 80 iff Fermat's Last Theorem was true. And it was less than two pages of code! The result was that in Ada 83 a compiler was not required to find an elaboration order that did not raise Program_Error, assuming one existed. In Ada 83 days, I gave a presentation at a SIGAda meeting in Dallas, I think. I had a very short package where the legality depended on whether or not the compiler generated code would raise Numeric_Error at run-time. In fact, the Verdix compiler compiled the program without error (and ran it without an exeception). The DEC Ada compiler declared the program illegal. And of course, both were right. We fixed that particular problem in Ada 95 with respect to Constraint_Error in 4.9(33-34). There are still many cases where an Ada compiler is allowed to reject a program as illegal if it will always raise Program_Error at run-time. It doesn't take much work to transform this rule into an oracle that solves the halting problem. Of course, that means that some programs will fail to compile in a reasonable amount of time--for any definition of reasonable. Why does this bother you? Remember I started this by saying that with Ada 95, we had deliberately accepted requiring all Ada compilers to solve NP-complete problems. We know that if someone wants to he can write a program that transforms any NP-complete problem into a bin packing problem, and then writes the bin packing problem as an Ada type with a representation specification. If that type declaration compiles, the actual layout of the type is a solution to the bin packing problem. The program containing the declaration just needs to print out the values of some static attributes. Now does that mean that any Ada compiler can solve any NP-complete problem in linear time? Not if you include the compile time. ;-) I don't recommend that as a way to solve most bin-packing problems. So why do we require Ada compilers to do it? Most bin packing problems have easy solutions, and if you have a record declaration it seems silly to say that we won't require compilers to solve the easy cases because there are some that are hard. Instead we warn the compiler writers about the tough cases, recommend an algorithm, and moved on. If the user overspecifies the record layout, it might take the compiler a while to find an acceptable solution. But we can't require that compilers violate G�del's Proof and we don't. We can't require them to solve the halting problem either, we just ask them to take their best shot. RM 1.1.5(5-6): "Errors that are required to be detected at run time by the execution of an Ada program; The corresponding error situations are associated with the names of the predefined exceptions. Every Ada compiler is required to generate code that raises the corresponding exception if such an error situation arises during program execution. If such an error situation is certain to arise in every execution of a construct, then an implementation is allowed (although not required) to report this fact at compilation time." Translation: There are some potential Ada programs that correspond to the halting problem. If such a program will always raise Program_Error, the implementation is ALLOWED to reject it at compile time. If the compiler can't decide, it may generate code which MAY raise Program_Error at run time for some inputs. So a compiler can reject programs that will raise Program_Error. But if the compiler can't decide whether or not the program will, it can drop back and punt. However, for any case where a compiler will ALWAYS reject program if it will raise Program_Error, you can do like the code above. Write a partial recursive function and put the code that will raise Program_Error after it. If the compiler says at compile time that the code will ALWAYS raise Program_Error, you know that your partial recursive function always halts. ;-) The program can be messy, but take a look at 4.9. That is the section that requires that static functions with static arguments be evaluated at compile time. If you find an instance that is as elegant as the four line instance I found in Ada 83, we will probably "fix" it in Ada 1Z. (And for the same reason, to improve portability between compilers.) But if it takes a 500 line program, we will probably leave it alone. -- Robert I. Eachus "The war on terror is a different kind of war, waged capture by capture, cell by cell, and victory by victory. Our security is assured by our perseverance and by our sure belief in the success of liberty." -- George W. Bush