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.2 required=5.0 tests=BAYES_00,INVALID_MSGID,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,4835289e9b0eb32d
X-Google-Attributes: gid103376,public
From: Ken Garlington <kennieg@flash.net>
Subject: Re: Critical code, Ada, Eiffel, Ariane etc.
Date: 1997/08/12
Message-ID: <33F0F421.6928@flash.net>#1/1
X-Deja-AN: 263801348
References: <Pine.SUN.3.91.970812160036.17653A-100000@erlang.praxis-cs.co.uk>
Organization: Flashnet Communications, http://www.flash.net
Reply-To: Ken.Garlington@computer.org
Newsgroups: comp.lang.ada
Date: 1997-08-12T00:00:00+00:00
List-Id: <comp.lang.ada>


Peter Amey wrote:
> 
> Recent, interesting, threads on programming safety-critical systems,
> language subsets, assertions, DBC etc. were kicked off by some kind
> remarks by Tucker Taft about SPARK, our secure, Ada subset.  Now that the
> dust has settled a bit I thought I would return to the original themes and
> explain why we believe SPARK addresses some of the issues raised.
> 
[much good discussion snipped]
> 
> The use of secure subsets and static analysis makes it harder to put bugs
> in the code; furthermore, it makes their early detection easier which
> offers dramatic savings in the integration test phase of a project (80%
> reduction in integration test costs has been quoted).  Furthermore, SPARK
> is not a toy, prototype or even partially completed piece of academic
> research - it is a real industrial strength tool usable, and used, on real
> projects.

As I recall, SPARK was used in the development of the C-130 airlifter
real-time mission-critical avionics, so I believe that it is quite
accurate
to say that SPARK has been used on "real" projects in an environment
very
similar to the Ariane 5.

I also think SPARK addresses many of my concerns with Eiffel-style
assertions
(and Ada-style exceptions), although there are still issues about the
number
and types of proofs generated. 

> Peter
> 
> P.S. As for Ariane: yes it is quite clear that a proof of absence of
> run-time errors using the SPARK Examiner would have revealed the
> circumstances under which the Ariane code would fail; however, given the
> real problem -- the decision that off-the-shelf code did not require
> re-test -- it is almost certain that no re-proof would have been required
> either!