Re: Safety-critical development in Ada and Eiffel

[Samuel Mize <smize@link.com>]

Marin David Condic, 561.796.8997, M/S 731-96 wrote:

> The Ariane software specifically and very deliberately *removed*
> the checks because of time constraints.

Correct me if I'm wrong.

My understanding from the previous threads was that there was
a specific management decision to not consider Ariane 5
requirements for the Ariane 4 INS design.  The check removal
was reasonable in the Ariane 4 context.

Then there was a specific management decision to not review
for Ariane 5 the requirements to which the INS was built, or
to retest it in the new conditions.

Given these decisions, the problem would not have been caught,
no matter what assertions were in the code.

Now, Meyer et al. never stated outright that using Eiffel (or
assertions) would have prevented the crash; they stated that
using Design By Contract (DBC) would prevented the crash.

This is trivially true.  Traditional methods of specification
review or design review or test would ALSO have prevented the
crash.  Saying "DBC could have prevented the crash" creates a
misleading suggestion that this demonstrates a DBC advantage
over other methods.

The Ariane crash proves that properly-managed DBC would be
better than DBMG (Design By Management Guesswork).  It neither
supports nor refutes the thesis that DBC is better than other
responsible/traditional engineering methods.

I can't say that Meyer et al. intended to imply otherwise, but
it is certainly a reasonable inference for the reader to draw,
given the paper.  That inference angered some people.

Samuel Mize