Re: Papers on the Ariane-5 crash and Design by Contract

[jezequel@irisa.fr (Jean-Marc Jezequel)]

In article <JSA.97Mar19144933@alexandria>, jsa@alexandria (Jon S Anthony) writes:
>In article <5gp3hd$i0l@mulga.cs.mu.OZ.AU> fjh@murlibobo.cs.mu.OZ.AU (Fergus Henderson) writes:

>> >Why is Eiffel saying assertions are a new tool?  C (and now C++) have been
>> >using #include <assert.h> for years?  Software engineers have been using
>> >assert macros to verify program limits are not exceeded. 

>> The major difference between C/C++/Ada assertions and Eiffel style
>> design-by-contract is that in the latter, the assertions are part of
>> the interface, not just embedded in the implementation.

>Well, in this particular sort of case, your claim here is not correct
>for Ada:

>subtype Bias_Constraint is Integer range Min_Bias..Max_Bias;
>
>function Convert ( High_Bias : Bias_Constraint ) return Integer;

>The asserstion is part of the interface, NOT the implementation.
>Further, to answer a point of Jean's, it will be inherited in any
>appropriate derivation case.  And certainly we could do the same for
>the post condition (the return subtype).

Yes, that's true for pre- and post that actually correspond to range
constraints. But remember that Eiffel pre- and post can be much more general
than that, including any arbitrary function call.
Also, how do you check/inherit your class invariants in Ada?
(this is a real question, I really don't know whether it is possible)

>Now, as John McCabe, Ken Garlington, myself and others have pointed
>out, none of this was (or is in any sense likely to be) sufficient to
>prevent the type of error exhibited by this example.  The required
>semantic context (scope of use, intended behavior, presumed
>environment, etc) is far to rich and complex to be dealt with by such
>rudimentary simple minded stuff as pre and post conditions on

In general, this may be true. But in this particular Ariane 501 crash, I maintain
that such "stuff" would have been  enough, for a team fully embrassing design by contract,
to specify this particular assumption. By the mere definition of design by contract, 
they should have done this. Then, with the process explained in another of my posts,
the constraint (along with many, many others) would have propagated to the boundaries of
the SRI module, as a constraint on the environment where the module could be reuse.

I would expect that you could agree with me on that, because it is just a bare bone application
of design by contract. What I concede you (Jon), is that the set of assertions
emerging at the SRI module level could have been so complex that it would have made
verification in the context of Ariane5 very costly in human ressources. 
I know that humans can fail, but I'm confident that, given enough ressources (and 
avoiding a 500M$ crash gives you some leeway) it could have been succesful.
You may disagree on this point, and we can stop this discussion by agreeing to disagree.

In the light of their very constructive posts and mails, I concede to Ken Garlington and 
Paul Dietz that re-testing of the SRI in the context of the Ariane5 trajectory would
not have been as hard as I have thought initialy. But in any case, the solution they propose
would have broken the idea of a black-box (integrating all the inertial hardware and software)
reuse, since you have to enter the black box to "feed simulated accelerometer signals into the
rest of the system". OK, I admit this is a bit of dialectics, but it still illustrates one of the
main point of the paper: beware of black-box reuse (aka component reuse), when the specification
is limited to routine signatures (a la CORBA).

>signatures.  *THE* most alarming aspect of this entire discussion is
>that many, including folks the caliber of Meyer and Jezequel, don't

Thanks for putting me on the same level as B. Meyer. I'm feeling flattered;-)


-- 
Jean-Marc Jezequel               Tel : +33 2 99847192         
IRISA/CNRS                       Fax : +33 2 99847171         
Campus de Beaulieu               e-mail : jezequel@irisa.fr 
F-35042 RENNES (FRANCE)          http://www.irisa.fr/pampa/PROF/jmj.html