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-Thread: f849b,b8d52151b7b306d2 X-Google-Attributes: gidf849b,public X-Google-ArrivalTime: 2004-01-11 20:36:19 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!wn13feed!worldnet.att.net!216.166.71.14!border3.nntp.aus1.giganews.com!intern1.nntp.aus1.giganews.com!nntp.giganews.com!nntp.comcast.com!news.comcast.com.POSTED!not-for-mail NNTP-Posting-Date: Sun, 11 Jan 2004 22:36:18 -0600 Date: Sun, 11 Jan 2004 23:36:16 -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.arch.embedded,comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems References: <3fe00b82.90228601@News.CIS.DFN.DE> <3ff18d4d.603356952@News.CIS.DFN.DE> <1731094.1f7Irsyk1h@linux1.krischik.com> <3ff1b8ef.614528516@News.CIS.DFN.DE> <3FF1E06D.A351CCB4@yahoo.com> <3ff20cc8.635997032@News.CIS.DFN.DE> 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-HOX4pLtED5sVhV/1k8A7LFIrffLhVpLi+m5hi0XAoUAKhxc1aC8VV09OGkd9q5Hw63jvrPDJVfIcjrX!wwp/6yiFIZjVT2JOzEOrydFmlPl9QlB5m4sIEYeFpLoWSG8MhY9GGQ3ZNjPv8A== 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.arch.embedded:7305 comp.lang.ada:4348 Date: 2004-01-11T23:36:16-05:00 List-Id: Chad R. Meiners wrote: > "Georg Bauhaus" wrote in message >>Are you sure you can say that a program that implements the Halting >>problem for a bounded Turing machine does not implement the same >>problem for a Turing machine? > > It depends what you mean by implement. I tend to think of implementations > as algorithms (which must halt). Therefore, since there is no algorithm > that satisfies the Halting problem's specification (it is undecidable), > there is not an implementation. If you want to define implementation as > something else (reasonable or unreasonable), all bets are off of course. Excatly, or anyother way of making my point. All physical machines have limits even if someone builds a self-replicating von Neuman system that keeps growing itself, it would be limited by the available matter in the universe. But in reality, for realistic time frames even the PC on your desk is a sufficiently close approximation to an infinite Turing machine. Does it really matter if I give you an implementation of the Halting problem for your PC that will always halt within a trillion years, instead of one that does not halt for some inputs? (And are you sure, if you had both in hand, you could tell which was which?) Anyone who works on compiler front end and language definitions has to be ready to dance with G�del, decidability issues and the whole nine yards. ANY compiler for a reasonable programming language, and even for some unreasonable ones runs right straight into G�del's proof. It either does not accept some legal programs, accepts some illegal programs, or never halts for some inputs. (And as many of you know, early releases of compilers tend to do all three.) G�del says that any Ada, C, C++, Fortran, or whatever compiler must have at least one of those three bugs in it. (In the Ada community, we aim for the first choice--that there will be some legal Ada programs that will be rejected due to implementation limitations.) I thought it was wonderful about a decade ago when we made a decision to require Ada compilers to solve NP-complete problems--and were honest about it. Record representation specifications can be only partially specified, and we require the compiler to find a legal layout if one exists. This is of course a bin packing problem, and with not much work ANY bin packing or knapsack problem can be mapped to an Ada record representation clause. However, for decades there have been requirements in the Reference Manual to solve the Halting problem, but we still dance around saying that. In Ada you can write expressions which will be evaluated at compile time, and the compiler must decide whether to accept or reject a program based on the results of those computations. (Did someone say G�del numbers?) I once wrote a joke compiler "benchmark" that used a series expansion to compute Pi to 50 places. (Our compiler compiled it correctly, but took about 20 minutes.) Actually Dave Emery and Rich Hilliard a few years later came up with an even more torturous compiler test. I think Dave wrote: type Positive_Integer is range 0..2**Integer'Last-1; by accident, and the Verdix compiler just kept churning away. (Of course the last expression was intended to be 2**Integer'Size-1 not 2**4_294_967_296-1.) I think a number of compilers now check for that error by bounding the terms if one gets too large. In this case once you get past 2**32 subtracting one can't bring the final result back in range, so you can declare an error and give up. But there are actually programs in the Ada test suite that depend on the fact that A*X-B*Y is a small number for some integers A, B, X, and Y > 1. With a computer you can hunt up some pretty nasty expressions that require several thousand digits in your arbitrary arithmetic package but the final result is say, 13. Why does Ada require this? Because it allows programs to be written using expressions meaningful in the problem domain. This goes back to the issue of making it easier for domain experts to validate designs and implementations. -- 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