Re: Design by Contract (was Re: Interesting thread in comp.lang.eiffel)

[Richard Riehle <laoXhai@ix.netcom.com>]

Having read this thread with interest, I have some views to share that will
probably annoy
people in both the Ada and the Eiffel community.

From everything I have seen, there is no clear picture that Design By
Contract would have
had any benefit for the Arianne V rocket.   Also, there is very little
anyone could have done
with standard Ada 83 to prevent the error.   In both cases, DBC and Ada
exception handling,
run-time checks were turned-off.   As noted by Ken Garlington earlier, even
a constraint error
check (Ada)  or an assertion check (Eiffel)  might have gone undetected in
this situation.

I think the DBC notion is an excellent one for lots of circumstances.  Maybe
not for a system
such as Arianne V.  In a system such as Arianne V, how many pre-conditions,
post-conditions,
and invariants are warranted?    Such a system typically goes through a
rapid series of state
transitions, each one governed by the previous state.   We design each
transition on the basis
of what we can predict about the current state along with what we can know
about the total
state of the system.

Under DBC we need to predict the possible states that need to be checked for
each transition
and guarantee some invariant for certain parts of the system.   We also need
to be sure the
assertion checking does not take longer than the processing required to make
the next state
transition.   In Industrial Engineering and Reliability Theory there is the
notion of 100% checking
for 0.001 % probability of error.    Do we want to do this 100% checking by
placing pre-,
post-, and invariant checks at every transition point or do we try to
predict where the system
is at risk and apply them only at those points.

Unfortunately, we in software have a poor track record for predictability.
In fact, some algorithms
are beyond our ability to predict through ordinary reasoning mechanisms.
For example, consider
Langton's Ant (you can read about it in Terry Pratchett' Science of
Discworld).   An Ant is on a
giant grid.  The squares on the grid can be either white or black.  The
algorthim is simple.  If the
Ant is on a white square, that square turns black and the ant proceeds to
the square on its left.  If
the square is black, the square turns white and the ant proceeds to the
square on its right.  (This is
a good programming exercise for students using a sparse matrix).   We can
easily declare assertions
for the states of each square, but cannot declare assertions for the state
of the entire grid.   Why?

According to Pratchett, it takes about ten thousand iterations of the
algorithm before any pattern begins
to emerge.  And that pattern is not predictable.   After ten thousand
iterations, a patter does emerge, but
there is no guarantee the pattern will not be broken after, say, twenty
million more iterations.

Large-scale software systems are often like this.  We can easily declare
simple little assertions that govern
the state of some part of the system, but it is impossible to cover all the
combinations of circumstances
at this level.   In both Eiffel and Ada we try to manage this complexity by
creating small, well-formulated,
easy-to-understand modules.   Even with that model of development, it is
still difficult to ensure that
the total state of the system (such as a rocket during launch) will not
enter into some odd combination
of circumstances that we could never predict.    We are not talking here
about the evil global variable.
We are talking about a real system in which the complexity requires multiple
engineers who must
communicate with each other and whose communication must make sense in terms
of the total product.

Assertions are not enough.  More important than the assertion is what to do
if the assertion fails.  Often,
we don't know what to do.   Again, Mr. Garlington laid out a list of common
responses to failure, but
there is no gurarantee we have selected the correct response.   No assertion
can guarantee that the
state to which we transition upon failure will be the correct new state.

Someone suggested an assertion based on some timing constraint.  That, of
course, would be very bad news.
The timing for different platforms will vary.  Instead, the assertion would
be based on the current state of
the module currently completing its operation, the postcondition along with
the state of the new module
(precondition) into which it intended to transition.   I raise this point
because it is not always clear how to
declare an assertion for a component.   The Arianne IV component might have
had a perfectly reasonable
"contract" based on its own timing mechanisms and could have failed to
protect Arianne V.  Remember,
assertions are checked at run-time, not at compile-time.   At run-time, in a
hard-deadline, real-time
system, there is very little time for the OOPS!  factor.

Both the Ada and Eiffel contributors to this discussion are endowed, I fear,
with an excess of hubris.  We
are so enamoured with our own notions of how to provide software excellence
that we oversimplify the
real issues related to this kind of software product.   Eventually, Design
By Contract, along with theorem
provers and other advances in computer science will move us all more in the
direction of more reliable
software, but it is not a finished idea yet.  It is a step in the right
direction.   Many of the ideas in Ada
will get better, and eventually Ada (as in the SPARK Examiner model already
in place) will benefit
from Design by Contract.   At present, SPARK is probably the best example of
Design By Contract,
but it is so conservative in its acceptance of contemporary ideas in
object-oriented programming that
many practitioners are reluctant to be so constrained.

One hundred years from now, those of our successors developing the
equivalent of computer software
will look back on our arguments with the same admiration we have for the
mathematicians in the time
of Charlemagne.

Arianne V was a big mistake that neither Eiffel nor Ada would have
prevented.  Let's get on with learning
how to make things work instead of beating up on each other about how much
better we are than the
other guy.

Richard Riehle
richard@adaworks.com