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-29 08:56:27 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!newsfeed.mathworks.com!wn14feed!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: Mon, 29 Dec 2003 10:56:25 -0600 Date: Mon, 29 Dec 2003 11:56:24 -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-AAzihXG+1+/GqfBCdIaLH0Z2Ln60PzaDbBva3oiK6Jkk+XUK6K4OF5w9Zeo3Hh6F89guOabyn5dAcYr!X7UbgiW5Gr6kLx08ksLlmD9Cl06g1iYmrUctOXuXtGdixhqOiArzVbes8sA01g== 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:6291 comp.lang.ada:3927 Date: 2003-12-29T11:56:24-05:00 List-Id: Chad R. Meiners wrote: > "Robert I. Eachus" wrote in message > news:ItOdncXDf7nrHnKiRVn-gw@comcast.com... > >>True in practice, and also in theory due to limits on memory sizes. > > I believe SPARK is a finite language. That is you can only declare finite > data structures. In general purpose languages you can declare infinite data > structures, which are needed to be Turing-Complete. Most compilers (and > computers) only support subsets of general purpose programming language ;-) I think we are agreeing violently. ;-) My point is that you can use external (from a SPARK viewpoint) storage to make SPARK Turing-Complete. For an example, consider an embedded system that includes a tape drive for data logging. The system as a whole is Turing Complete, given an operator to change tapes, but it wouldn't normally be used in that way. So you would be able to prove that a package that used the tape drive to implement a stack was correct, but you couldn't validate programs that used the tape as an unbounded store. Once you get into this situation, which I have run into on several projects you have to decide where to make the cut. I remember one particular (pre-SPARK) Ada project where we validated that the program would not fail if it ran out of logging space, and that the amount of logging space available met the system spec. We just had to live with the fact that the logging requirement was somewhat arbitrary. -- 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