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

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

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 7754 bytes --]


Don Harrison wrote:
> 
> Before getting into this, let me say that I acknowledge that specifying
> assertions is largely futile unless they are tested. [Well, that's not
> strictly true because they have documentation value (though not much if not
> correct) and do help the developer become more aware of their assumptions.]
> 
> Ken Garlington writes:
> 
> :From this, I deduced (possibly erroneously) that Design by Contract
> :helps in the
> :precise specification of components, and that the implementation
> :language has
> :nothing to do with this specification.
> 
> At the risk of putting words into their mouths, I think Bertrand and Jean-Marc
> may mean Design by Contract in its richest sense as available in Eiffel and
> Sather rather than an impoverished version of it.

Exactly. This contradicts an earlier post by Mr. J�z�quel, to which I
was responding.

> If they are speaking of it
> in this sense, this statement is certainly true of any language that supports
> it fully. It's also true that the same benefit is available to a lesser degree
> in languages that support it in an impoverished form. The truth is, Ada
> developers use Design by Contract (of a kind) liberally as I'll explain below.

However, the paper (and Mr. Meyer, in posts to this thread) make it
clear that
Ada (including Ada95) is not adequate for Design by Contract.

> 
> They ought to make no excuse for believing in using the best available tools
> for that's what software engineering is about - using the best tools for the
> job in the most effective way to produce high quality software. This is the
> essence of genuine Design by Contract.
> 
> I now use contracting liberally in my own Ada development (well, I've always
> used subtypes, but now use more general assertions as well) and I'm convinced it
> more than pays for itself in reduced integration time. Granted, they take extra
> effort to design and debug but it's more than offset by easier testing.
> 
> So, what is meant by "Design by Contract in its richest sense". Assertions
> that are:
> 
>   1) Built-in because
>      - It's easier to automatically document the specification.
>      - It's easier to visually differentiate assertions from mandatory code.
>      - Developers are more likely to use them, IMO. ["IMO" only because, while
>        obviously true, it is difficult to prove.  :( ]
> 
>   2) General because
>      - They allow you to specify at any level of abstraction (high to low).
>      - They allow you to specify virtually any specification (anything
>        expressible as a boolean expression - not just range constraints on
>        discrete types).
> 
>   3) Inheritable because
>      - The specification is propagated into descendants causing it to be
>        automatically reused and enforced. Because descendants are forced to
>        honour contracts, you can be confident they will behave correctly
>        (provided the software is tested, of course).
> 
> :To summarize from the post, they are:
> :
> :1. Being ABLE to specify the assumption does not mean that the
> :   assumption WILL be specified.
> 
> True. You can put an electric drill in someone's hands and they can
> (without plugging it in) gouge a hole by manually turning it, but it would be
> a whole lot easier if they just turned the power on and used it properly.

I'm afraid I don't understand this argument. You consider writing code
easier than not writing code?

> 
> :There is evidence it would not have
> :   been specified, even using Design by Contract.
> 
> I consider this unlikely. Assuming a reasonably-designed system, a contract
> testing for this abnormal behaviour would be expressible at some level of
> abstraction.

You are free to consider this unlikely. However, there are specific
statements
in the final report that support this assertion. See the referenced
earlier
post. If you have evidence to the contrary, you may want to address this
point in more detail.

> 
> :2. SPECIFYING the assumption does not mean that a violation of the
> :   assumption will be DETECTED. There is evidence that it would not
> :   have been detected before flight.
> 
> Agree. An assumption will only be detected if tested.
> 
> :3. Even if the problem was DETECTED, there is no guarantee that the
> :   appropriate ACTION would have been taken. There is evidence that
> :   an incorrect action would have been taken.
> 
> Agree. Appropriate action will only be taken if the exception handler is
> designed to cater for the misadventure.
> 
> However, also true is the fact that if you specify contracts you will detect
> *as many* and, likely, *more* errors (providing testing is adequate etc. etc.)
> than if you do not specify them.

Yes, absolutely.

However, again, my comments are directed at the paper Mr. Meyer and Mr.
J�z�quel regading a *specific* application of contracts in a *specific*
context. Based on that *context*, I believe their conclusions are in
error.
 
> 
> Now, before explaining this, let's clear something up. Many Ada developers
> already use (a specific kind of) Design by Contract day-in-day-out without even
> realising it. Some contributors to this thread have indicated that Ada
> programmers specify their own contracts by declaring Ada subtypes. But subtypes
> are not the only way they use contracting. They also use a swag of pre-defined
> contracts provided by the language environment. To identify them, we need to
> take a look at Ada's predefined exceptions. We see that each one specifies a
> specific kind of contract (sorry this is only Ada-83 - there are probably more
> in Ada-95):
> 
> 1) constraint_error: a contract specifying that
>    - The allowable bounds of a discrete type (subtype, array index) will not
>      be exceeded, or
>    - A record variant will only exist for a specific discriminant value
>    - etc.
> 
> 2) numeric_error: a contract specifying that
>     - A floating point value will be within the bounds of the type.
> 
> 3) program_error: a contract specifying
>    - The unit ('object') containing the operation called will have been
>      initialised, or
>    - A function will return (a postcondition)
>    - etc.
> 
> 4) storage_error: a contract specifying
>    - That a task will not exceed its allocated storage, or
>    - The heap will not exhausted
>    - etc.
> 
> Well, you get the picture. Probably, the reason some Ada developers have
> trouble seeing how they can benefit from Design by Contract is because they're
> oblivious to the fact that they already use it liberally in the form of
> predefined contracts (and reap the benefits of it)!
> 
> While it's good that Ada is rich in specific pre-defined contracts, it
> disappoints in that it doesn't offer the full power and flexibility of
> *user-defined* contracts in the way Eiffel does. If it did, then it would
> be easier to specify the more general kind of assertion that would expose
> the kinds of dysfunction that may go unnoticed in an assertion-less Ada
> program.

Again, in the *context* of the paper:

1. As the paper explicitly states, Ada was adequate for this type of
error.

2. The paper does not make the case that "making it easier to specify"
the
   right assertion would have led to saving the Ariane 5, as it claims.
   As you noted, there are critical holes in the path from "able to
   specify" to "fault detected" which would have avoided the crash.
   Apparently, I think there's more holes than you, but we appear to
   agree there were sufficient holes.

> 
> Don.
> =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
> Don Harrison             donh@syd.csa.com.au

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