Re: Safety-critical development in Ada and Eiffel

[Joachim Durchholz <joachim.durchholz@munich.netsurf.de>]

Ken Garlington wrote:
> What if the mistake is in your code, not the calling code?

There's always an end to the chain in buck-passing. If the mistake is in
our code, we obviously have to fix it. DBC is not a silver bullet, it is
just a way of unambiguously distributing responsibilities (preconditions
to the caller, postconditions to the callee - and the callee is *not*
required to check its preconditions in its code).
Or, if the system must be fail-safe, the buck is passed up to some
routine that just takes note of the software failure and tries something
else (or detonates the rocked).

> 1. My_Aircraft.Mine is correct. (How is this determined?

Proofreading.
However, assertions are (hopefully) on a higher level than the program
code, so the task of the proofreader becomes easier by that level.

>    Do assertions
>    have
>    assertions?

In Eiffel, no. Assertions are on a higher level of reasoning than the
program code itself. The advice is to write simple assertions (again to
make proofreading easier).
Personally, I'm not totally sure wether this will properly scale up to
arbitrarily large systems. Adding assertions to assertions, however,
adds a second layer of checking (which would have to be read and
understood by the proofreader), so assertions on assertions aren't too
useful anyway.

> 2. Assume_Control is not called again with the same aircraft between
>    the
>    pre-condition and My_Aircraft.Add.
> 3. Release_Control (I propose this as the opposite of Assume_Control)
>    is
>    not called between My_Aircraft.Add and the post-condition.

This is taken care of.
For single-threaded applications, the problem cannot arise anyway.
For multi-threading, only a single procedure may execute at any time for
a given object.

> 4. There are no errors from other sources (e.g. extraneous code,
>    higher-tier
>    documentation miscommunications).

You might formalize the higher-tier documentation as deferred (abstract)
Eiffel classes. The concrete system is built by deriving from the
deferred classes. DBC makes sure that the concrete classes will abide by
the contracts in the high-level specification classes.
Of course this does not preclude other communication problems. But
there's no silver bullet for this.

> Also: If the post-condition fails, who provides the corrective action?

A postcondition failure means the routine is wrong; as it already has
terminated executing, it cannot take corrective action.
So the caller is left to deal with the broken contract - either by
failing its own contract (the default reaction), or by taking corrective
action (catching the exception and trying some other approach).

> Also: If My_Aircraft.Add is provided by a different programmer/team
> than
> Assume_Control, does it call My_Aircraft.Mine (or a subset thereof)?
> Why
> or
> why not?

I'm having trouble understanding the situation you're thinking of here.
Usually a class is written by a single programmer/team.
Besides, wether a routine is called once or twice doesn't seem related
to who wrote it, so I'm rather confused here...

> Also: it's my understanding that DBC requires My_Aircraft.Mine be made
> available
> to the client of Assume_Control (no private pre-conditions). Is this
> the
> case
> here?

Yes.

> Why or why not?

The caller must be able to check wether it has fulfilled all
preconditions. It can do so only if all features used in preconditions
are available to him.

> Does this mean that the pre-condition may be
> checked twice
> before each call?

Yes. (Only once with precondition checking turned off.)
However, this is misleading. If PBC is in place, you don't have to write

  do_something (My_Aircraft: AIRCRAFT) is
  do
    if MyAircraft.Mine then
      -- do something with My_Aircraft
    else
      -- declare error
    end;
  end; -- do_something

Instead, you write

  do_something (My_Aircraft: AIRCRAFT) is
  require My_Aircraft.Mine
  do
    -- do something with My_Aircraft
  end; -- do_something

which is shorter, and clearly separates the "defensive programming" part
from the really useful code.

> However, these results seem to be limited to making sure the code does
> what
> you thought it was supposed to do.
> How are the other failure sources
> handled?
> ...
> Also, given that Meyer claims the "most important" effect of
> assertions
> is manual analysis (see section 3.1 of same paper), shouldn't you be
> doing this
> anyway (in addition to any executable testing)? If you're not
> reviewing
> these manually, why not?

DBC doesn't handle external failure sources. It is there to make sure
that the code does what it's supposed to do.
As a very useful side effect, it also seduces the programmer into
getting a clear picture of what the routine is actually supposed to do
(something many programmers really need).

Regards,
Joachim
-- 
Please don't send unsolicited ads.