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: 2004-01-10 22:53:40 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!small1.nntp.aus1.giganews.com!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 00:53:34 -0600 Date: Sun, 11 Jan 2004 01:53:33 -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> <5802069.JsgInS3tXa@linux1.krischik.com> <1072464162.325936@master.nyc.kbcfp.com> <1563361.SfB03k3vvC@linux1.krischik.com> <11LvOkBBXw7$EAJw@phaedsys.demon.co.uk> <3ff0687f.528387944@News.CIS.DFN.DE> <1086072.fFeiH4ICbz@linux1.krischik.com> <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> Organization: LJK Software 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-fTOZYwrYMOt8RtdStDeWlUXCXHgFWED6Kwp0WTMery9UrVEwu3bH1fXRxHixF7bU7kQVckZPIxAQfym!BlDE5itOyBWgBwVfkM7lUzN0CQfeMT36HvNryc75SOAXuNOqWsBBdEj9v5BAiw== 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:7251 comp.lang.ada:4325 Date: 2004-01-11T01:53:33-05:00 List-Id: Hyman Rosen wrote: > Robert I. Eachus wrote: > >> The Airbus 320 should bury the idea that theorem provers can result in >> safe software. > > > It's always been my contention that writing the specifications which you > will then prove that a program obeys is exactly as hard as writing the > program itself. Depends on where you draw the line. I have been on Ada projects where more that 85% of the effort and budget went into requirements and design (through to detailed specifcations, which included writing the Ada package specs). All of them finished on time and under budget. If you do the design right, writing, debugging and testing the package bodies is easy. But I don't recommend that you contract the coding to Primate Programmers, Inc. (PPI): http://www.newtechusa.com/ppi/pressroom.asp#higher ;-) -- 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