Re: Interresting thread in comp.lang.eiffel

["Ken Garlington" <Ken.Garlington@computer.org>]

"David K Allen" <dkallen@visi.com> wrote in message
news:BRab5.418$6E.94216@ptah.visi.com...
> "Ken Garlington"  wrote
> > It keeps getting ignored (I suspect because the question can't be
> answered),
> > but I'll post this example again. The DbC specification for a module is
> > given below. I feel fairly confident that this is considered a good
> quality
> > example by at least one acknowledged Eiffel/DbC expert.
>
>     ;)
>
> >
> >    convert (horizontal_bias: INTEGER): INTEGER is
> >       require
> >          horizontal_bias <= Maximum_bias
> >
> > If, as you say, this would cause the project team to go get information
> they
> > did not already have, then explain what information it would require and
> > why.
> >
> > (My analysis of this DbC specification is in the link noted above).
>
> First, I don't think the  authors intended that this one function would
have
> prevented the entire disaster.
> If they meant that, then I must join you in your critique.
> I think they were trying to give an illustration that would convey the
> approach of DBC in the context of the disaster. But I can see you were not
> impressed <grin>.
>
> Second, as you point out in your critique, the error occurred prior to
where
> this function would have been used (conversion from FP to Integer).  But
if
> you accept my previous remark, then that is not the point of their
example.
> I admit they chose poorly if they were intending to persuade you, who have
> such a command of the details.
> But for conversation sake,  and to illustrate the usefullness of DBC,
let's
> assume that the flaw occured within 'convert' above.  Otherwise, I can't
> help you see how DBC helps me think and work.

As I note in the paper, you can reasonably generate examples where DbC
helps. However, the examples provided to date are not, IMHO, germaine to the
specifics of the Ariane 5 case. Here's an even more interesting aspect:
Given that the author of the proposed contract appears to be showing an
example specific to the Ariane 5 case, and given that he _knew_ a priori
where the error resided, and given that (he claims) the information provided
in the inquiry was sufficient for him to understand the nature of the
problem, he STILL BLEW IT. He failed to write a contract that addressed the
problem. This should give anyone pause as to the ease of establishing such
contracts.

More to the point, I have yet to see anyone write an Eiffel contract that
_does_ address the Ariane 5 example -- particularly in a portable and
readable manner. Again, this is even after we (apparently) fully understand
the conditions we're trying to denote. I'm not claiming that it's
impossible, but I suspect that it will be more complicated than a one-liner
(as the person who posted the "tangent" contract hopefully also discovered
:).

> Yes, I know - the reason for this jointly agreed decision was cited as
> maintaining CPU performance. My only claim is that if DBC were part of the
> coding culture, it would have been less likely that that decision would
have
> been "jointly" agreed to.

However, you have to consider that at least some of the "joint" decisions
(in particular, the extermely critical one regarding the SRI specification)
were quite likely made by personnel that would have been unaware of the
software team's decision to use DbC, much less used those contracts in their
decision making process.

> If I were working on high-risk stuff with a team
> of others trained in DBC, I can't see that we would reach a consensus to
> ignore the warning of a precondition.  It just would not be done without
> management overriding us.

Again, the part of the statement that reads "a team of others trained in
DbC" is critical to the argument. If you are dealing with a software system
on a standard hardware platform, where the domain of interest is mostly
software-specific, this is reasonably likely. However, the SRI environment
(and, more to the point, the rocket environment containing it) is not likely
to meet this criteria.