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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,f039470e8f537101
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-07-22 02:02:55 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!logbridge.uoregon.edu!newsfeed.vmunix.org!fu-berlin.de!uni-berlin.de!adsl-213-200-246-247.cybernet.CH!not-for-mail
From: Vinzent Hoefler <ada.rocks@jlfencey.com>
Newsgroups: comp.lang.ada
Subject: Re: Ariane5 FAQ
Date: Tue, 22 Jul 2003 11:00:48 +0200
Organization: JeLlyFish software
Message-ID: <bfiujt$f9lj1$2@ID-175126.news.uni-berlin.de>
References: <mailman.26.1058753354.24167.comp.lang.ada@ada.eu.org>
 <1058799152.775376@master.nyc.kbcfp.com>
 <bfh2gb$eeiv4$1@ID-175126.news.uni-berlin.de>
 <1058810510.375902@master.nyc.kbcfp.com>
 <bfhaed$e786b$1@ID-175126.news.uni-berlin.de>
 <1058813341.841940@master.nyc.kbcfp.com>
 <bfhe55$eqglr$1@ID-175126.news.uni-berlin.de>
 <1058816605.566685@master.nyc.kbcfp.com>
 <bfhjjr$eftm1$1@ID-175126.news.uni-berlin.de>
 <3F1CC443.FD2BA89D@adaworks.com>
Reply-To: v.hoefler@acm.org
NNTP-Posting-Host: adsl-213-200-246-247.cybernet.ch (213.200.246.247)
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: quoted-printable
X-Trace: news.uni-berlin.de 1058864574 16045665 213.200.246.247 (16 [175126])
X-Newsreader: Forte Agent 1.8/32.548
Xref: archiver1.google.com comp.lang.ada:40615
Date: 2003-07-22T11:00:48+02:00
List-Id: <comp.lang.ada>

Richard Riehle wrote:

>Vinzent Hoefler wrote:
>
>Bertrand Meyer published a controversial article suggesting
>that, had they used design by contract ( a la Eiffel) this could
>not have happened.

Probably you also read
<URL:http://www.flash.net/~kennieg/ariane.html>?

>  While I don't agree that Eiffel would have
>been better for the job, a contract model such as that found in
>SPARK might have been successful in detecting the design
>error early on.

I would even doubt that, because the design was based on the
assumption that certain values would not exceed their range. The
programmers knew it wouldn't happen in normal operation, so I think it
is very likely they would have told the prover, it won't do that. So
it would have changed exactly nothing at this point.
But, *perhaps* it would have been slightly better documented because
someone should justify such a decision in the proof-process and so
some people might have taken a closer look at these assumptions and
then concluded "Houston, we've got a problem." ;) But that's just a
guess. Nobody seemed to check the requirements changes between the IRS
for Ariane 4 and 5 anyway...


Vinzent.

--=20
Parents strongly cautioned  --  this  posting  is  intended for mature
audiences  over  18.  It  may  contain some material that many parents
would not find suitable for children and may include intense violence,
sexual situations, coarse language and suggestive dialogue.