Re: Safety-critical development in Ada and Eiffel

[donh@syd.csa.com.au (Don Harrison)]

Ken Garlington wrote:

:Don Harrison wrote:
:> 
:> What we want is a way to signal to the caller that they've made a mistake and
:> need to take corrective action. 
:
:If they don't know to check that they might have made a mistake, 

They *do* know because they get an exception.

:how do they know what corrective action they should take?

To determine the right corrective action, they determine which specific 
(sub-)expression triggered the violation and work out the cause by conventional
means, namely logical deduction.

:If the erroneous code is reused in another application, doesn't it carry
:its error along with it?

Yes, that's why it's important to fix it. :)

:What if the mistake is in your code, not the calling code?

The context we're dicussing is a precondition, so I assume you mean a mistake 
in the precondition. This will be obvious from the fact that the call is valid. 
This is what I mean about the code proper validating assertions. (See my previous 
posts for details).


:> What about case 2)? Here, we want to check that the work we delegated was
:> done properly and acheived what we set out to do. In this case, we can
:> perform some checks and raise and exception against ourselves to force us
:> to fix the problem (possibly by delegating)..
:> 
:>   procedure Assume_Control (Aircraft: Aircraft_Type) is
:>   require not My_Aircraft.Mine (Aircraft)
:>   begin
:>     ...
:>     My_Aircraft.Add (Aircraft);
:>   ensure My_Aircraft.Mine (Aircraft)
:>   end;
:> 
:> which is our final solution. What we are now left with is a component of
:> software that we know can only be executed under the intended conditions and
:> can guarantee producing the required results.
:
:Assuming...
:
:1. My_Aircraft.Mine is correct. (How is this determined? 

Joachim has already mentioned code inspection. 

Also, if Mine is called anywhere in the code proper of the system and it has 
its own assertions, it will be validated by them. However, these lower-level 
assertions won't be evaluated as part of higher-level assertion evaluation.

(For details, see OOSC-2, Chapter 11 - "Design by Contract: Building Reliable
Software", Page 400 ff.)

In this sense, I suppose you could say there are "assertions about assertions" (meta-assertions). They help where they're needed most - where assertions are 
abstracted using boolean functions.

:Do assertions have assertions? 

See above.

:What happens if an assertion's assertion fails, and how
:is
:   it distinguished from an assertion failure?)

Because assertion checking is turned off during assertion evaluation, this
doesn't happen.

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

Neither of these concurrency issues exist under SCOOP because the runtime system 
automatically locks objects on behalf of the thread using them. It's simply 
impossible to have concurrent access to an object by multiple threads. 

(For details of object locking under SCOOP, see OOSC-2, Section 30.6 - 
"Accessing separate objects", Page 982 ff.)

Ada, in contrast, does allow this - for example, if tasking is used in isolation. 
To overcome this deficiency, you have to either roll-your-own object protection
(using semaphores, for example) or use protected objects. Using Ada protected 
objects is fine, but they lack the flexibility of Eiffel separate objects.

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

I've already covered the case of extraneous code in a previous post. 

WRT documentation-related problems, these are outside the scope of any runtime 
error checking mechanism. DBC is *almost* a silver bullet but not quite. :)

:Correct?

All of these issues are either non-issues or already catered for.


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

During development, you, the designer of the code (or your delegate) by fixing 
the problem. Additionally, in the case of critical software, you can add a
rescue clause (exception handler) to keep the show on the road in production. 

: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)? 

It doesn't matter. What's your point?..

: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? Why or why not? Does this mean that the pre-condition may be
:checked twice
:before each call?

(Joachim's already answered this).


:> We now move on to the next
:> component and repeat the process. Step-by-step, piece-by-piece we construct
:> our reliable ATC system. We did so *incrementally* through a divide-and-conquer
:> strategy and by being demanding in what we expected of callers and demanding
:> of ourselves in producing the correct results.
:
:However, these results seem to be limited to making sure the code does what
:you thought it was supposed to do. 

Yes?..

:How are the other failure sources handled?

Clairvoyance. :)  Seriously, we already know that DBC can't identify all sources
of error. Other classes of error may be identified through other means that 
you're already well acquanted with.

:> Sorry if this is a bit Mickey Mouse for some, but some may find this helpful.


: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)? 

Absolutely! For critical application, you want to do whatever you can to 
improve reliability - including manual analysis.

:If you're not reviewing these manually, why not?

I would.


Don.
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
Don Harrison             donh@syd.csa.com.au