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

[jsa@alexandria (Jon S Anthony)]

In article <slrn5jmbhv.7k9.kennel@lyapunov.ucsd.edu> kennel@nospam.lyapunov.ucsd.edu (Matt Kennel (Remove 'nospam' to reply)) writes:

> :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.  
> 
> Of course static type constraints are a form of 'precondition', namely
> "the object being referred to by this reference, or in this variable is
>  one of these types".
> 
> By that measure C++, C, and Pascal, and maybe even Fortran have assertions. 

Yes, I would agree with that.  Also note that while subtypes are
indeed "primitive" in comparison to Eiffel capabilities, their limits
can be (and often are) computed at runtime.  For example:

    subtype Current_Constraint is integer range Current_Min .. Current_Max;

where both Current_Min and Current_Max are functions.


> It is often useful and powerful to program in a style in a
> statically typed language where important information is encoded
> into types, but this is not a full substitute for Eiffel's
> additional capabilities.

Absolutely agreed.


> Whether or not it would have done so in the rocket crash is another
> story.

Check.  The main thing to note in regards to this point is that

  a) the sort of assertion capability called out in the M&J paper
which supposedly could have helped is nothing more (or less) than an
Ada subtype constraint.

  b) the practitioners knew all about this capability and even used
it in places.

  c) the particular case in point was _proven_ to be not possible
_within_ the contextual environment intended for the use of the
component.

  d) given c) there is no good reason (no reason even) to include such
an assertion and in fact very good reasons to _not_ include it.

  e) for those who think d) is dumb, please note that this sort of
thing is standard practice in _real_ engineering - lest nothing would
be buildable and/or useable.

To draw an analogy, someone who is designing a wing notes that the
context of its use will be that of standard A to B general aviation
flights.  The context also requires all sorts of practical things like
weight limits, cost limits, etc. for the sort of use it will have.
Now, such an environment does not require unlimited style acrobatic
flight or some such.  Nor does it assume that the pilots will
intentionally fly into category 6 thunderstorms.  The G loads of the
environment are will within limit loads of +3 and -1 (ultimate loads
of +4 and -2).

Now, under such circumstance why would the designer require that the
wing shall meet limit loads of +10/-10?  The attitude of some people
here seems to be "of course it should be built with such capability -
some fool _might_ try to fly acro with the plane it is on or maybe go
into such storms".  But that's not the context of use and in the
intended area of use, the cost of such a thing will be much more than
another perfectly suitable wing with the appropriate assumed limits.
It will likely be much heavier as well, and with less usable space for
fuel cells.  This would reduce practical useful load and range in any
airplane using it.  What's more, it is always possible that someone
would exceed +10/-10 as well.  So where do you stop?

Now, where is this sort of contextual information in such real
engineering designs?  In the "code" - i.e., actual example?  No way.
That's way to easy to miss.  It's in the associated specifications,
blueprints, and documentation - including all the way down to the user
(pilot operating handbook).

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