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

["Joachim Durchholz" <joachim dot durchholz@halstenbach.com>]

Howard W. LUDWIG <howard.w.ludwig@lmco.com> wrote:
> David Kristola wrote:
>
> > What kinds of DbC things could i do in Eiffel that i
> > can't do in Ada with pragma Assert and good typing?

Stuff like
  my_parame /= Void
or
  find_minimum_in (h: HEAP)
  require
    not h.is_empty
or
  solve (q: QUADRATIC_EQUATION)
  require
    solvable (q)
or
  sqrt (r: REAL): REAL is
  require
    r >= 0.0
or
  log (r: REAL): REAL is
  require
    r > 0.0
(try to put both the preconditions for sqrt and log into a range type
<g>).

It's just more flexible. In fact Eiffel has no range types; the
understanding is that contracts properly include them. (Personally, I
tend to disagree but I can live well with just contracts.)

> How are the "require" and "ensure" blocks handled--as
> executable code at run-time,

Usually, provided that you have switched run-time checking on (e.g.
because you're testing your code - it's not usually done in production
code).

> as compiler-checking,

In principle, yes. No such tool has yet been built though; it would
require
a) a quite powerful inference engine and
b) some way to allow programmers to help with inferences if the engine
doesn't come up with a proof, or
c) meaningful warnings that pinpoint the problem so that the appliation
programmer either knows what to change in his code or can prove validity
by hand.

It would be an interesting large project to do that. Most inference
engines are built for academic languages.

> or
> simply as comments to support humanoid review or automated
> checking by tools other than the Eiffel compiler?

This usage is always a part of DbC. It tends to be more important than
the checking aspects.

> How does the caller handle the
> verification of the preconditions if they are spelled
> out in [only] the callee?

As David wrote, it's usually done by the compiler which compiles
everything in one large blob (no separately compiled libraries).
But that's just an accident of current Eiffel implementations. For
example, for

  sqrt (r: REAL): REAL is
  require
    r >= 0.0

an Eiffel compiler could emit assembly code like this:

_checked_sqrt:
  <establish stack frame>
  <evaluate "r >= 0.0"
  <jump to _start_sqrt if test came out true>
  <raise exception in caller>
sqrt:
  <establish stack frame>
_start_sqrt:
  <start code for foo's normal body>

That way, it's the caller's choice: if it calls _checked_sqrt, it's
getting the precondition checking, if it calls sqrt, it's getting no
precondition checking.
The code for raising an exception in the caller should just unwind the
stack and raise the exception, while the code for raising a
postcondition exception does not unwind the stack. (The exact details of
exceptions depend on the presence of debuggers etc., so I won't go into
detail here.)

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

I have used DbC in practice, and it is immensely useful. I used to write
"defensive code" in the past, and always had the problem that I never
knew what my code should do if it really detected a problem. Then I had
the same checking in the callers... and lots of trouble whenever the
specifications of the code changed.
Today, I do the same defensive programming and put it into the
preconditions. However, I don't code them in the caller anymore (so the
caller doesn't have to worry whether he really understood the
documentation - the callee should do all the relevant checks), the
caller doesn't have to worry about the inefficiencies of defensive
programming (just switch assertions off for the code that you're
confident in).

Regards,
Joachim
--
This is not an official statement from my employer or from NICE.
Reply-to address changed to discourage unsolicited advertisements.