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-7-bit X-Google-Thread: f849b,b8d52151b7b306d2 X-Google-Attributes: gidf849b,public X-Google-Thread: 103376,a00006d3c4735d70 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-12-28 17:29:27 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!small1.nntp.aus1.giganews.com!border1.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, 28 Dec 2003 19:29:26 -0600 Date: Sun, 28 Dec 2003 20:29:25 -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> <3FE026A8.3CD6A3A@yahoo.com> <3bf1uvg2ntadvahfud2rg6ujk24sora6gr@4ax.com> <2u3auvogde8ktotlaq0ldiaska3g416gus@4ax.com> <20619edc.0312221020.3fd1b4ee@posting.google.com> <20619edc.0312222106.3b369547@posting.google.com> <45cs9hAbLc6$EAAx@phaedsys.demon.co.uk> In-Reply-To: Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Message-ID: NNTP-Posting-Host: 24.34.214.193 X-Trace: sv3-Gov7PptwcqyxFbLdccsyHvdHhCb/Aw/yq06JdPFzw/y/64ynSLCVYE/V0s6cIeWTeYeirkezact5Yev!xJvk+/Ra/cNjN9TVo/SjKroDO4BRY+pQNXlwVqNmC7c+2cbGxKuxykh/1MB02g== 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:6247 comp.lang.ada:3906 Date: 2003-12-28T20:29:25-05:00 List-Id: Chad R. Meiners wrote: > Rice's theorem states this. It is a result of the undecidablility of the > Halting problem, and it is also related to Godel's incompleteness theorem. > I would suggest taking a class on computation theory, but it might suffice > to read a book on computation theory and work through the problems. ... > No it isn't a contradiction. SPARK is not a general purpose language; it is > a special purpose language (SPARK is not Turing-Complete hence Rice's > theorem doesn't apply to it), which is designed to facilitate deep static > analysis. True in practice, and also in theory due to limits on memory sizes. But if you were to write a SPARK program that was an interpreter for a general purpose language, verification would only result in proving that the interpreter worked correct and say nothing about programs in the interpreted language. Not how you would use SPARK in any case, but it is worth remembering. Just as I can write Ada programs that are not SPARK programs but can statically proven to halt, or I can write an Ada program for which no such proof is possible. SPARK just provides a convenient way to write programs that can be proven correct, and to automate much of the proof. In C it is much, much harder to write programs that can be proven correct, but it can be done. One way is with an Ada to C translator. If I had to produce a large safety-critical system for a chip which did not have an Ada compiler, using an Ada to C translator (several exist) and the SPARK tools might be a decent alternative to an Ada port. In practice for the small programs that are common on 8-bit chips, I find it easier to validate the generated code to the original requirements. -- 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