Re: Critical code, Ada, Eiffel, Ariane etc.

[Ken Garlington <kennieg@flash.net>]

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!