Re: Safety-critical development in Ada and Eiffel

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

Ken Garlington wrote:

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

Yes, but we're not talking about writing the code. We're talking about execution. 
Even Smalltalkers can't write and execute at the same time. :)


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

DBC won't fix the errors for you. :)

No tool can *think* for you. DBC does help identify and localise errors, but 
you're the one who must solve them. 


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

No. If an error doesn't exist, it can't be ported.


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

The developer running the program - by thinking.


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

I'm not suggesting it should be.


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

We're talking about different things. See the OOSC-2 reference and my comments
following for details..

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


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

In theory, yes. In practice, I would expect SCOOP implementations to provide 
greater flexibility through optimisations (See below).

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

Optimisations could allow multiple concurrent queries (reads). The important 
is that exclusive access is *theoretically* guaranteed. What happens in practice
doesn't matter so long as it's safe.


:> (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! 

Incorrect.

:Protected objects, for example, would allow concurrent reads
:if no timing issues result!

See above. You lose flexibility with protected types because they're not  
inheritable and can't be used polymorphically.

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

No, I said something else. 


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

Both.

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

I agree this is an important area.


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

I don't see any problem with using it as both.


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

Who said anything about clients? I said the designer of the code containing 
the postcondition - that is, the *supplier* in Eiffel parlance.

My original example, reinserted..

:  procedure Assume_Control (Aircraft: Aircraft_Type) is
:  require not My_Aircraft.Mine (Aircraft)
:  begin
:    ...
:    My_Aircraft.Add (Aircraft);
:  ensure My_Aircraft.Mine (Aircraft)
:  end;

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

Correct me if I have this wrong, but you seem to be worried about too few checks
and too many checks. 

WRT too few checks, it's always the responsibility of the client to make sure 
the precondition is met. So, a check will always be made.
 
WRT too many checks, an implementation may optimise out any redundant checks 
- for example if a precondition check is already done by a caller. This minimises
the number of redundant checks.

:If both teams do the call, this is not nice from a
:efficiency standpoint.

See above.


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

The difference is it does a better job of it.

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

Not entirely true. DBC can highlight specification/design inconsistencies.
(See my previous posts). Otherwise, I agree. 

:it has limitations with respect to implementation language, 

More accurate is to say that most languages provide limited support for it.

:it's not clear that it scales well, 

Not true. 

:and it doesn't appear to be internally complete (big on error detection 
:mechanisms, not much on how to derive the particular error sources, 

That's because they're typically blindingly obvious! Why? Because error detection
is more localised.

:and not much on what to do after the error is detected, for example).

Again, this is usually blindingly obvious. 


All of these points have been made before. 


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