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

[jsa@alexandria (Jon S Anthony)]

In article <5gjoel$jre$1@quasar.dimensional.com> rkaiser@dimensional.com (Richard Kaiser) writes:

> In article <332D113B.4A64@calfp.co.uk>, Nick Leaton <nickle@calfp.co.uk> wrote:
> 
> >2) Design. Writting assertions makes design easier. This is a personal
> >observation and harder to justify. I find being clear about what
> >something does helps clear up what I am doing. Having complex
> >preconditions is not a good idea, again you probably don't have the
> >right structure.
> 
> The code is going to assert "I will not run correctly in this new rocket?"

No.  And this is not the sort of thing that simple pre and post
conditions is going to help you with.  It's disingenuous to say
otherwise.  In fact, while this paper is fairly good in its analysis,
it is extremely poor in its conclusion.  Here's the relevant bit:

 "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:"

Well, the facts indicate that the answer should be "highly UNlikely".
Why?  Because the language used _does_ have such capabilities.  Here's
the relevant Eiffel:

convert (horizontal_bias: INTEGER): INTEGER is 
              require 
                    horizontal_bias <= Maximum_bias 
...


The *exact* analog with the *exact* same capabilities in Ada is:

function Convert ( Horizontal_Bias: Integer ) return Integer is
    subtype Bias_Constraint is Integer range 0..Maximum_Bias;
    Require : Bias_Constraint := Horizontal_Bias;
...


So, the _only_ evidence we in _fact_ have, is that this sort of
capability DOES NOT help in this sort of scenario.  And actually, that
should not be very surprising.  It is not even particularly
interesting.

Here are a few more bits which just don't hold up:

   "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."

Exactly the same in Ada, including the above type of constraint.

   "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."

Exactly the same in Ada, including the above type of constraint.

   "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."

Exactly the same in Ada.  Assuming you actually _write_ the assertion.

   "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."

Exactly the same in Ada.  Assuming the constraint was written.

But, the constraint was not written.  This despite the fact that the
language, Ada, was fully capabale of _explicitly_ expressing the
assertion with clear and easily seen demarcated code.


 Nick sez,

> >There are other more complex parts to Eiffels assertion system, in
> >relation to inheritance, and soon in relation to parallel processing.

Yes, but the bald fact of the matter is, even the most capable aspects
of Eiffel assertions are just too rudimentary to be of any use in this
sort of scenario.  They do not have anything even remotely like the
semantic context capabilities needed to address this problem.


/Jon
-- 
Jon Anthony
Organon Motives, Inc.
Belmont, MA 02178
617.484.3383
jsa@organon.com