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-17 16:20:32 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!c03.atl99!sjc70.webusenet.com!news.webusenet.com!pd7cy2so!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: Sat, 17 Jan 2004 18:20:28 -0600 Date: Sat, 17 Jan 2004 19:20:27 -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-oquZh7CuHlR05MoWkTWw5Kl+PYSuEpGT5PNmDxcf99JeGjSKfQaVTDdw1bNRQMEWhWnYtIwrdyJb67v!7bTB9Za1l0WhEjxuBH1z+jmArxAArsgdQQ9lFZ9nPrjlMb5vn9Dnf34cCftmDQ== 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:4510 Date: 2004-01-17T19:20:27-05:00 List-Id: Robert A Duff wrote: > That was simply a mistake in the wording of the Ada 80 manual. > Not a property of "all useful programming languages". Ah, but the mistake required all valid Ada 80 compilers to solve the halting problem. The solution was to remove that requirement. And that is my point, when specifying programming languages such issues are a (maybe not common but occasional) occurance. >... 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. > No. The Ada RM carefully distinguishes between compile-time and > run-time errors, and compilers are certainly *not* allowed to "reject as > illegal" programs that will (or might) raise exceptions. "Reject as > illegal" means "refuse to run it". I chose my words carefully. RM 10.2 (27) "The implementation shall ensure that all compilation units included in a partition are consistent with one another, and are legal according to the rules of the language." Often failure of the compiler to determine that there is a consistent elaboration order means that there is no valid elaboration order. But we allow the compiler to reject a program if it didn't find a valid order. Why? See above. Requiring the compiler to find a valid order requires solving the halting problem. (Note that an implementation MAY choose an order that cannot be shown to be inconsistant, and provide code that causes Program_Error if access before elaboration occurs.) But if there is no valid elaboration order, and the compiler detects that, the program is illegal. > No. There is no requirement that Ada compilers pack records optimally. > A rep-clause specifies the layout of components specified. The compiler > must check that these do not overlap. That can be done in linear time. > The rest of the fields can be placed anywhere the compiler likes, and > that also can be done in linear time. There is no requirement to > (optimally) solve the bin-packing problem. There is no requirement to OPTIMALLY solve the bin-packing problem, true. But if there is a size clause applied to the record, then we do require the compiler to find a consistant solution if one exists. >>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. > > This translation is wrong. What the RM says is that compilers can print > out a message. It cannot "reject" such a program; it must run it. > Note "of a construct" in the RM wording. For example: > > X := 0; > if Some_Condition then > X := X / X; -- divide by zero > end if; > > Every execution of the construct "X / X" will surely raise C_E, because > it divides by zero. The compiler is allowed (but not required) to tell > you that. It has no obligation to prove that Some_Condition will > sometimes be True. I agree with you on this case. I was thinking about the case where the implementation detects that there is no LEGAL elaboration order. Such a program is illegal and may be rejected. If it cannot be detected whether a valid elaboration order exists, then the compiler MUST generate code to raise Program_Error if an illegal elaboration order occurs. The "classic" case is a program that has a library unit that reads in input from the user, (in the sequence of statements in the program body) and either makes or doesn't make a call to the main program before it is elaborated. > No. Compilers must *not* reject the above divide-by-zero program -- > they must allow it to be run. Even if it said "if True then" or "if > False then", it's still a legal Ada program, and we can tell that > without invoking Halting Problems. Agreed. > Static expressions cannot contain recursion (or even loops), so I don't > see what this has to do with Godel or the Halting Problem. > > It's certainly true that some static expressions can require a huge > amount of memory to evaluate. E.g., "2**(2**(2**(2**32)))". I expect > any compiler to complain about that. It's a capacity limitation, but I > don't see how it has anything to do with Godel's theorem. Go back and read G�del. He uses a clever encoding of a logical calculus in the factors of (large) numbers (G�del numbering) to show that arbitrary statements can be encoded in an arithmetic formula with a limited number of terms. That showed that recursion is not necessary to cause a language to accept contradictory statements. -- 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