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 20:35:12 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!logbridge.uoregon.edu!canoe.uoregon.edu!elk.ncren.net!solaris.cc.vt.edu!news.vt.edu!msunews!not-for-mail From: "Chad R. Meiners" Newsgroups: comp.arch.embedded,comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems Date: Sun, 28 Dec 2003 23:34:01 -0500 Organization: Michigan State University Message-ID: 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> NNTP-Posting-Host: arctic.cse.msu.edu X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2800.1158 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1165 Xref: archiver1.google.com comp.arch.embedded:6260 comp.lang.ada:3914 Date: 2003-12-28T23:34:01-05:00 List-Id: "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 ;-) > 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. Well if you had some nice properties about the interpreted language then the verification of the interpreter would imply that those program apply to the program while they are being interpreted. I know---I am nitpicking, but I have been trained to. > Not how you would use SPARK in any case, but it is worth remembering. I believe the SPARK examiner is written in SPARK. ;-) > 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. I completely agree. I just get excited about SPARK because it is one of the few formal tools situated toward the end of the verify/validation chain. For instances for a formal methods class, I used Promela and LOTOS to prove a theorem for a safety property about a set of traffic lights for a one lane bridge. With SPARK I was able to able to prove that the premise of that theorem was satisfied by the traffic controller program that I wrote. > In C it is much, much harder to write programs that can be proven > correct, but it can be done. I agree. However, directly working with proofs about programs written in C would probably not be a process that you could pick up in a week to finish a class project ;-) > 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. This really isn't writing C programs to be proven correct. It is generating them as an intermediate representation. Once the C code is compiled, you can still use the practice that you suggested below. > 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. A wise practice considering that compilers have bugs. However, the point of verifying that SPARK code meets validated requirements is to detect errors sooner to simplify the later stages of development. Hopefully once you VV the SPARK program, your task to VV the generated code is simplified. -CRM To reply by email, change the "hotmail" to "yahoo".