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-29 01:24:53 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!bloom-beacon.mit.edu!nycmny1-snh1.gtei.net!washdc3-snh1.gtei.net!news.gtei.net!ngpeer.news.aol.com!newsfeed1!bredband!uio.no!feed.news.nacamar.de!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, 29 Jul 2003 10:06:05 +0200
Organization: JeLlyFish software
Message-ID: <bg5a1g$l7sjg$1@ID-175126.news.uni-berlin.de>
References: <3F200AD0.94F79098@adaworks.com>
 <e2e5731a.0307241721.a6eae4e@posting.google.com>
 <7u9Ua.13412$634.10307@nwrdny03.gnilink.net> <3F215120.1040706@attbi.com>
 <1059151910.357790@master.nyc.kbcfp.com>
 <e2e5731a.0307251844.7ea4dab4@posting.google.com>
 <bDTUa.6456$AO6.976@nwrdny02.gnilink.net>
 <e2e5731a.0307271419.4390a02c@posting.google.com> <ud6fvzbzc.fsf@xsol.com>
 <3F248CEE.5050709@attbi.com> <3F25FB81.A81694FA@adaworks.com>
 <K9oVa.12850$AO6.11742@nwrdny02.gnilink.net>
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 1059466096 22278768 213.200.246.247 (16 [175126])
X-Newsreader: Forte Agent 1.8/32.548
Xref: archiver1.google.com comp.lang.ada:40928
Date: 2003-07-29T10:06:05+02:00
List-Id: <comp.lang.ada>

Hyman Rosen wrote:

>Richard Riehle wrote:
>> I am thinking here of SPARK.
>
>The Ariane 4/5 problem had nothing to do with proving the
>correctness of a program. Had they used SPARK, they would
>have informed the verifier of the presumed limits of the
>input, and the verifier would have happily verified that the
>program was correct.

Yes, that's probably true.

>But if the Ariane 4 code had carried the specification limits
>within it, as DbC, or as SPARK assertions, or as range checks,
>perhaps someone might have noticed that the Ariane 5 failed to
>meet those constraints.

That isn't much different from SPARK where you should justify such
decisions for the verifier. I don't think either method would have
helped, because nobody seemed to look at the requirements at all.


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.