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,f039470e8f537101
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-07-28 23:06:34 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!cyclone.bc.net!in.100proofnews.com!in.100proofnews.com!cycny01.gnilink.net!cyclone1.gnilink.net!spamkiller2.gnilink.net!nwrdny02.gnilink.net.POSTED!53ab2750!not-for-mail
From: Hyman Rosen <hyrosen@mail.com>
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US;
 rv:1.5b) Gecko/20030723 Thunderbird/0.1
X-Accept-Language: en-us, en
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Ariane5 FAQ
References: <mailman.26.1058753354.24167.comp.lang.ada@ada.eu.org>
 <wqkTa.18742$0F4.18264@nwrdny02.gnilink.net>
 <pan.2003.07.23.00.31.01.14991@mail.utexas.edu>
 <1058968422.225561@master.nyc.kbcfp.com> <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>
In-Reply-To: <3F25FB81.A81694FA@adaworks.com>
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <K9oVa.12850$AO6.11742@nwrdny02.gnilink.net>
Date: Tue, 29 Jul 2003 06:06:34 GMT
NNTP-Posting-Host: 162.83.157.195
X-Complaints-To: abuse@verizon.net
X-Trace: nwrdny02.gnilink.net 1059458794 162.83.157.195 (Tue,
 29 Jul 2003 02:06:34 EDT)
NNTP-Posting-Date: Tue, 29 Jul 2003 02:06:34 EDT
Xref: archiver1.google.com comp.lang.ada:40927
Date: 2003-07-29T06:06:34+00:00
List-Id: <comp.lang.ada>

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.

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.

And if they had tested it properly, such checks would have
served to pinpoint where the problem lay.