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

[Robb Nebbe <nebbe@iam.unibe.ch>]

Bertrand Meyer wrote:
> 
> Is it ever possible  to have a technical discussion without
> resorting to insults? Jon S. Anthony finds it productive to write,
> about one of my earlier messages:

Yes, he was insulting; however, apparently you did not read and
understand his post. (which is admittedly hard when you have been
insulted) He does have a valid point that neither you and Jean-Marc
Jezequel have not addressed. 

Your article in IEEE Computer clearly demonstrates that you do not
understand what actually happened and how it relates to the Ada
programming language. You do diagnose the problem correctly but your
suggestions for possibly avoiding the accident, in the context of a
correct understanding of what really happened, come across as very
naive. (which is probably the reason that you have Jon Anthony so upset
in the first place)

The important text from Jon Anthony's post (that you edited out) is the
following:

> Ada _has_ assertions.  Their form is not of the same syntactical look
> as Eiffel's.  So what?  They take the form of constraints, in
> particular (wrt to the case at hand) subtype constraints.  They are
> _not_ as flexible or full "featured" as Eiffel's but they are
> certainly there and in the Ariane case, they are every bit as capable
> as Eiffel's.  

Notice that Jon limits the scope (very clearly in my opinion) to say
that in the Ariane case they are as capable as Eiffel's. I.e. the
use of Eiffel in the Ariane --even with its undeniably more general
support for assertions-- would not have helped one bit.

In your article you include the following section:

> Does this mean that the crash would automatically have been avoided
> had the mission used a language and method supporting built-in
> assertions and Design by Contract? Although it is always risky to
> draw such after-the-fact conclusions, the answer is probably yes: 
>
>       Assertions (preconditions and postconditions in particular)
>       can be automatically turned on during testing, through a
>       simple compiler option. The error might have been caught then. 
>
>       Assertions can remain turned on during execution, triggering
>       an exception if violated. Given the performance constraints
>       on such a mission, however, this would probably not have been
>       the case. 
>
>       But most importantly the assertions are a prime component of
>       the software and its documentation ("short form", produced
>       automatically by tools). In an environment such as that of
>       Ariane where there is so much emphasis on quality control and
>       thorough validation of everything, they would be the QA team's
>       primary focus of attention. Any team worth its salt would have
>       checked systematically that every call satisfies the
>       precondition. That would have immediately revealed that the
>       Ariane 5 calling software did not meet the expectation of the
>       Ariane 4 routines that it called.

The problem with this section is that constraint checking (Ada's
simple support for assertions about scalar types amoung others) was
turned on during execution and this resulted in the exception. I would
assume that they were also turned on during any testing since turning
them on only during execution would be foolish. Finally the evaluation
to see if any exceptions were possible --the equivalent of making
sure every precondition is satisfied-- was done for the Ariane 4 and
based on this analysis several "assertions" were protected.

The real problem was that this analysis was not done for the Ariane 5.

This was truly beyond the scope of a programming language and comments
to the contrary are at best uninformed. Your "probably yes" is based
on an a provably incorrect understanding of the actual situation.

Other than this major blemish I found the article to be very well done.
It is definitely a resuse error. However, since Eiffel doesn't offer
any substantially better facilities than Ada _in_this_particular_
situation_ the claim that Eiffel (since they seem to have used an
appropriate method for Ariane 4) would probably have made a difference
is understandably infuriating to Jon, to whom it is obvious that you
don't know enough about Ada to recognize that your claim is bogus.
(that still doesn't excuse him being rude but it does explain it)

Robb Nebbe