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

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

David Kristola <David95037@See-My.Sig> wrote:
> On Sun, 16 Jul 2000 12:12:10 -0700, Joachim Durchholz wrote
> (in message <8kt1eb$34jh1$1@ID-9852.news.cis.dfn.de>):
>
> > David Kristola <David95037@See-My.Sig> wrote:
> >> On Thu, 13 Jul 2000 11:12:53 -0700, Joachim Durchholz wrote:
> >>
> >>> or
> >>> find_minimum_in (h: HEAP)
> >>> require
> >>> not h.is_empty
> >>
> >> Depending on the implementation of the heap, this too would
> >> probably cause some sort of exception to be raised if the
> >> heap were empty.
> >
> > The difference is that the exception will happen before the routine
> > is even called. The responsibility for the exception will clearly
> > be the caller's.
> > If the exception happens somewhere inside the routine, you need
> > another analysis step to find out which part of the code is really
> > responsible for the problem.
>
> Perhaps it is my coding style, but (in this limited case) i would
> consider it the responsibility of the caller to handle the exception.

Oh, this is not a limited case. The vast majority of failed assertions
is in precondition checks (well, at least during debugging.)
In nearly all cases, the caller needs to be fixed. (There is the rare
occurrence that a precondition was needlessly strict. If we own the
library with the callee, we take the opportunity to weaken the
precondition in this situation.)

> There is nothing find_minimum_in can do if the heap is empty.  To me,
> that is even an unstated but obvious contract.

The difference is that the contract is explicit.
Besides, the contract isn't obvious. The routine could reasonably return
some minimum value if the heap is empty. In that case, we'd have one
precondition less and one postcondition more.

> This is not to say
> that it is not worth stating obviously and in a way that can be
> checked by a compiler.  This particular example is perhaps a little
> simple.  Certainly there are plenty of others that are not so
> obvious, where a formally stated precondition adds to the
understanding.

It's usually the other way round: Writing preconditions can relieve you
of verbiage in the description. Say you have a routine like this in
FILE:

  read (offset, number_of_bytes: INTEGER; target: BUFFER)
    -- Read 'number_of_bytes' bytes into 'target', starting at file
    -- offset 'offset'.
    -- File must be open.
    -- Do not try to read past end-of-file.

This can be rewritten in a more concise and formal way as

  read (offset, number_of_bytes: INTEGER; target: BUFFER)
    -- Read 'number_of_bytes' bytes into 'target', starting at file
    -- offset 'offset'.
  require
    must_be_open: open
    dont_read_past_eof: offset + number_of_bytes <= file_size + 1

where 'open' and 'file_size' are other functions of FILE.

The first interface is what you usually read in some software
description. It leaves much to desire: there is no indication what will
happen if the preconditions aren't fulfilled, and it doesn't tell the
programmer what exactly has to be done to make sure that the call will
not fail.

The second interface is clearer. The reaction to a failed precondition
will always be an exception, or unspecified behaviour if checking is
switched off. This is quite harsh, but people tend to write short
preconditions; if clients of 'read' want a less strict contract (say,
reading past EOF fills the rest of 'buffer' with null bytes or whatever)
then bugger the routine author.
It's also *much* more precise: the preconditions leave no question open.
The caller must make sure that the 'open' query on the FILE returns
True, and he must fulfill some precisely defined numeric inequation on
'offset' and 'number_of_bytes'. The caller can then republish the same
contract on its own interface (if the caller has such a things as
'offset' and 'number_of_bytes'), or it can translate the preconditions
to some higher abstraction. For example, a class that embodies a file
with fixed-length records might have this routine:

  read (record_number: INTEGER; target: FIXED_LENGTH_RECORD)
  require
    must_be_open: open
    dont_read_past_eof: record_number <= number_of_records
  do
    internal_file.read (record_number * record_size, target.size,
target)
  end

  open: BOOLEAN
  do
    Result := internal_file.open
  end

  number_of_records
  require
    must_be_open: open
  do
    Result := internal_file.number_of_bytes div record_size
  end

I'm leaving out details like checking that the file size is an integral
multiple of record_size, a check that will probably be done in the
'open' routine; to ensure that this is always true, we can write this:

  invariant
    integral_records:
      internal_file.number_of_bytes mod record_size = 0

Together, these specifications make sure that FILE's 'read' routine will
never be called with inappropriate parameters.
Well, unless I overlooked something - it's a bit late right now and I
don't have the time to check that the preconditions percolated up
precisely. In a real-life situation, I'd make sure that this really
holds up, either by extensive testing, or by code review; in an ideal
world, I'd ask an inference engine whether the 'read' call guarantees
all its preconditions.

> Ada also does not provide for the inheritance of contracts.  That is
> a very interesting aspect of Eiffel.

Actually this is the main concept in Design by Contract.
It's essentially the Liskov Substitutability Principle applied to
preconditions and postconditions: If you have a variable of type PARENT,
and assign to it an object of type CHILD, then everything should work as
expected - in other words, all routines in CHILD must honor all
contracts that the precursor routines in PARENT offered. (CHILD may
offer more value: its routines may require less of the caller, i.e.
loosen up the precondition, or they may guarantee more, i.e. specify a
stricter postcondition.)

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