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

[Ken Garlington <GarlingtonKE@lmtas.lmco.com>]

Jon S Anthony wrote:
> 
> 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.

Exactly. It has been implied that, with Design by Contract, that the
reasons _not_ to include an assertion are mitigated to the extent that
just about every conceivable assertion is routinely included in systems
designed with this methodology. I could be easily convinced that there
are more explicit assertions in a DBC program than an Ada program, based
on the extra expressive power in Eiffel specifications. However, if a
programmer sees the violation of an assertion as highly improbably, I
would expect it would not get written regardless of the language used.
I would be interested in evidence to the contrary.

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

--
LMTAS - The Fighter Enterprise - "Our Brand Means Quality"
For job listings, other info: http://www.lmtas.com or
http://www.lmco.com