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

["Howard W. LUDWIG" <howard.w.ludwig@lmco.com>]

David Kristola wrote:

> On Tue, 11 Jul 2000 6:14:44 -0700, Ken Garlington wrote
> (in message <85Fa5.11419$7%3.818927@news.flash.net>):
>
> > convert (horizontal_bias: INTEGER): INTEGER is
> >       require
> >          horizontal_bias <= Maximum_bias
>
> I'm not saying that Design by Contract is a bad thing,
> but i hope there is a whole lot more to it than this
> example seems to say.  I saw a similar example for a
> formatted comment in Java that can be checked by a
> tool.
>
> Ada does the above by using a subtype that is limited
> to Maximum_Bias.  (The Java example had a post condition
> contract saying that the out parameter would be
> positive, again, the Ada solution is to use a subtype).
>
> What kinds of DbC things could i do in Eiffel that i
> can't do in Ada with pragma Assert and good typing?
>
> How can i use the concepts of DbC to make better Ada
> code?
>
> Thanks,
>
> --
> --djk, keeper of arcane lore & trivial fluff

I would like to add my own questions--actually add some
specificity to David's questions.  I have never coded in
nor learned Eiffel before, so _some_ of these concepts
are new to me and I am a bit confused.  In particular:

How are the "require" and "ensure" blocks handled--as
executable code at run-time, as compiler-checking, or
simply as comments to support humanoid review or automated
checking by tools other than the Eiffel compiler?  The
reason I ask is that I have read in this thread and in
skimming through OOSC that in a contract, using Eiffel/
DbC principles, a caller is responsible for verifying
the preconditions (the "require" block) and the callee
is responsible for verifying the postconditions (the
"ensure" block).  How does the caller handle the
verification of the preconditions if they are spelled
out in [only] the callee?

I'm interested in the overall DbC philosophy on this
topic of verifying contracts, the Eiffel implementation,
and what and how much can be done similarly in Ada
implementations.  The DbC distribution of responsibility
for satisfying contracts seems to be clean--somewhat
different from what is usually done, and I'm not totally
convinced yet that it is the best way to go, but _at least_
it is a well-defined way, which is better than having no
way and taking a haphazard approach.  Range-checking on
Ada subtypes seems to take the DbC approach in general,
but full-fledged assertions would seem to execute wherever
they are written, which imposes most of the burdens,
whether pre- or post-conditions on the callee.

Any clarification would be most appreciated.

Howard W. LUDWIG