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: 103376,15b0ab6fa90f819d X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2004-04-14 07:20:16 PST Path: archiver1.google.com!news1.google.com!news.glorb.com!newsfeed3.easynews.com!easynews.com!easynews!border1.nntp.sjc.giganews.com!nntp.giganews.com!local1.nntp.sjc.giganews.com!nntp.comcast.com!news.comcast.com.POSTED!not-for-mail NNTP-Posting-Date: Wed, 14 Apr 2004 09:20:15 -0500 Date: Wed, 14 Apr 2004 10:20:14 -0400 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.lang.ada Subject: Re: "Tracking the Blackout bug" References: In-Reply-To: Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Message-ID: NNTP-Posting-Host: 24.147.90.114 X-Trace: sv3-NlV+TtdZSECbscu4Azt1D1gJu9BedNkALrZNP2LvrzeJthAgWf6x7WDWx3XWmrSVUpeL8Lh9cwVBzYi!8sluIHhAz/i/YlCvZ9dzoTK11KI2akBCWkm/1kknmw5wJjx4AfcuLoxLMPr27g== 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.lang.ada:7092 Date: 2004-04-14T10:20:14-04:00 List-Id: Peter Amey wrote: > The developers did NOT do everything they could. They could have used > the Ravenscar profile in Ada; they could use RavenSPARK; they could have > done some model checking of the concurrent parts of the program. They > did NOT test exhaustively because it is impossible (/exhaustingly/ I am > willing to believe). And software doesn't HAVE to be cr*p! I totally agree, using Ada to write the software would not have prevented the problem, it just would have made it obvious. (Hmmm. How do we handle an exception in the alert system?) Using SPARK of course, would have prevented the problem. (If you can't prove it doesn't raise exceptions or have race conditions, it isn't SPARK.) -- Robert I. Eachus "The terrorist enemy holds no territory, defends no population, is unconstrained by rules of warfare, and respects no law of morality. Such an enemy cannot be deterred, contained, appeased or negotiated with. It can only be destroyed--and that, ladies and gentlemen, is the business at hand." -- Dick Cheney