Re: Safety-critical development in Ada and Eiffel

[Ken Garlington <kennieg@flash.net>]

Don Harrison wrote:
> 
> 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.

Not when they're _writing_ the code, unfortunately. Remember, the
assumption is
that the caller (directly or indirectly) made a mistake to cause the
exception
in the first place. However, in your scheme, you're trusting them to
take the
right corrective action to a problem that they may have unintentionally
caused
in the first place!

Human lapses in judgement aren't usually confined to a few-second
bursts. If
they make an invalid assumption in their algorithm, they're probably
going to
maintain that same invalid assumption when writing their
exception-handling
code.

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

This brings up the second point. Why would a methodology/language go to
great lengths to _detect_ errors, but completely punt ("use conventional
means") to determine what to do _afterwards_?

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

Doesn't this erode the argument of using Eiffel to support reuse, if
errors
are so easily ported between applications?

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

Your code thinks the call is invalid. Who decides otherwise?

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

See my arguments related to manual inspection as the only safeguard
against
errors in large systems.

> 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, other posts have said that assertions shouldn't have
assertions.
What is the DBC position?

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

So, if an object is referenced by a thread, no other operations
associated with
the object can be called (object-locking, as opposed to
operation-locking)?
Doesn't this cause a few latency problems? For example, it's usually OK
for
multiple reads to occur concurrently, so long as no write is in process.
SCOOP
only permits sequential reads?

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

Just the opposite! Protected objects, for example, would allow
concurrent reads
if no timing issues result!

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

Right - you said that you assume this won't happen. I was just noting
this
fact.

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

Is DBC a methodology, or a "runtime error checking mechanism"? I
certainly know
methodologies that will help uncover extraneous code, and
requirements/design
issues. In fact, some methodologies emphasize the ability to manage
requirements
and design, since that's where many of the really difficult errors
emerge.

> 
> :Correct?
> 
> All of these issues are either non-issues or already catered for.

I'm not sure that saying "DBC won't help with this" is the same as
saying
that they are "non-issues."

Someone needs to decide if DBC is a coding guideline or a software
development
methodology. My concern is that it is touted as the former, but used as
the
latter.

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

So, the client has to figure out what to do if your code fails? I
wouldn't
be inspired to confidence to reuse such code!

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

It matters a lot! Again, if each team assumes the other does the call,
this
is bad news. If both teams do the call, this is not nice from a
efficiency
standpoint.

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

But DBC is advertised as identifying other sources of error (e.g., the
code
does what's it's supposed to do, but only in a given environment).

> Other classes of error may be identified through other means that
> you're already well acquanted with.

Furthermore, the classes of error to which DBC is limited are
well-covered
through other means (beat to death, in fact). So, I'm still at a loss to
see what DBC brings to the table here. It doesn't address my main
problem
(requirements/design faults), it has limitations with respect to
implementation
language, it's not clear that it scales well, and it doesn't appear to
be internally
complete (big on error detection mechanisms, not much on how to derive
the
particular error sources, and not much on what to do after the error is
detected, for example).