Re: Interresting thread in comp.lang.eiffel

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

OK, here's a clarification:

Legal contracts between companies are usually negotiated.
Technical (DbC) contracts are negotiated when the callee is written.
They are no re-negotiated when the code is reused (unless the code is
opened up for redesign).
There is a connection between DbC and legal contracts. You can use DbC
contracts to specify the interface of a module (be it hardware or
software). If a failure related to the module occurs, DbC contracts will
tell you whether the error was in the module or outside.

David Gillon <david.gillon@baesystems.com> wrote:
>
> The need for information
> exchange for DBC would first have had to be pursued up multiple levels
> of the sub-contractor management tree until a level was reached at
which
> the release of information could be sought, and then on the contractor
> side chased back down the tree until someone was found who could
explain
> what was wanted. Think Dilbert 1 trying to have a technical discussion
> with Dilbert 2 by passing verbal messages through ten layers of pointy
> haired bosses each.... The assumption that this would logically result
> in the contractor 'gladly complying' doesn't necessarily reflect what
> happens in reality.

Actually DbC helps with this. Dilbert 1 will ask his manager "I need the
contract for this-and-that piece of software/hardware", and there isn't
much that the PHBs can misinterpret. DbC is a very formal tool - it's
just boolean expressions.

> One thing I'm still waiting to hear in this discussion is how Eiffel
> would handle a temporal constraint of the type 'Signal A will be
updated
> with its new value within 2.5 ms of a change to any of its source
> inputs'.

The method to get this type of DbC is always the same:
1) Imagine what you need to verify the constraint in a software that's
rigged for verifying this constraint. If this requires remembering a
series of measurements, do that.
2) Write a boolean-valued function that verifies the constraint.
3) Put that function into whatever assertion you have to check.

There's no magic involved here. It's just the same as ordinary software
instrumentation.

The real difference is that DbC assertions come with clearly defined
guidelines:
1. If a preconditions fails, look for the error in the caller. (If you
find that it's really a problem in the callee, it's time to review your
contracts.)
2. If a postcondition fails, look for the error in the callee. (If you
find that it's really a problem in the caller, it's time to review your
contracts.)
3. If writing code for a subclass, don't require more in your
preconditions than the base class.
4. If writing code for a subclass, don't ensure less in your
postconditions than the base class.
5. Have a software environment that can selectively switch checking on
or off, on a by-class (or even by-routine) basis.
6. Use the assertions to document the assumptions in your code.
7. Write the assertions before you code. You're lazy, so you'll write
shorter assertions as these are done first, and it will be easier for
you to write an extra code of line to support a simpler (and thus more
robust) interface semantics than to first write some code and then
document all the hidden assumptions.
8. Write the assertions by going down the interface specifications of
your software and transforming every specification into a boolean
function that tests whether your software is conforming to the
specification. (Ideally the specifications should already come in the
form of assertions, but you can't have everything.)

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