Re: Safety-critical development in Ada and Eiffel

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

Ken Garlington wrote (with deletions):

:Don Harrison wrote:

[...]

:> No. If an error doesn't exist, it can't be ported.
:
:Consider the Ariane case. The error didn't exist in the original
:environment
:(Ariane IV). The error only occured during execution in the Ariane 5
:environment (a little too late to fix, unfortunately). Basing your
:argument
:on execution means that any latent error in the system, which might be
:caught in other methodologies through the use of analysis and reviews,
:will
:be missed using DBC/Eiffel.

I disagree. I'll explain below..

[...]

:> :> (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.
:
:Eiffel separate objects always lock the object. Ada protected records
:can lock the
:object for a given operation or not (at the designer's preference), 

IMO, this is something the designer is better off leaving to the compiler as 
it can be expected to do a better job of it. If Ada protected types allow 
the designer to explicitly leave objects unlocked (which doesn't appear to 
be supported by the Ada95 Rationale), then they are more permissive but 
in a detrimental way, IMO.

:can requeue requests, 

IMO, the situations in which you would use "requeue" are better handled by 
designing differently - perhaps by using an additional class. If anything,
"requeue" probably encourages poor design.

:etc. 

What are these?

More choices for the designer usually means additional
:flexibility, I would think.

Drawing some inspiration from Robert Dewar, "flexibility" and "permissiveness" 
have at their root the same meaning but differ wrt the user perceives a benefit 
or detriment respectively.

[...]

:> :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.
:
:However, there is a serious problem when practitioners use it (and
:discuss it) in terms of the former. Note the number of times in this
:post, for example, that DBC has been described in terms of concrete
:capabilities when the subject is code execution, but only vaguely
:(if at all) when described as a methodology..

Your basic worry seems to be that DBC doesn't appear to be an all-embracing, 
formal software engineering methodology.

At this stage, I think you're right. I think the reason why is that DBC 
probably hasn't been used in the context of *formal* software engineering. 
If it had, then it would have been integrated with other complementary 
reliability-enhancing techniques. 

IMO, a methodology centred on DBC, would also include stuff about systematic
testing of components. In the Ariane case, this might involve bolting an IRS
onto some test bench and stimulating it with Ariane 5 data. This may require
simulating the surrounding environment. Then, any assertions assuming Ariane 4 
inputs would be violated (as would the Ada constraint_error). In general, 
the extra checking afforded by DBC would mean more bugs would be identified 
than if it wasn't used. (Yes, I know there is no difference wrt the one that 
caused the failure.)

[...]

:> :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.
:
:I saw your previous posts. I quote from the line above:
:
:  "WRT documentation-related problems, these are outside the scope of
:  any runtime error checking mechanism. DBC is *almost* a silver bullet
:  but not quite."

Right person, wrong quote and wrong context. If it's any help to you, the 
comments I'm referring to were about mutually validating requirements. I 
acknowledged not all documentation errors were covered. 

[...]

:> :it's not clear that it scales well,
:> 
:> Not true.
:
:Can you provide evidence to the contrary?

I've already covered this. Nick's experience also endorses it.

[...]

:> :and not much on what to do after the error is detected, for example).
:> 
:> Again, this is usually blindingly obvious.
:> 
:Any time someone says something is obvious, without any evidence or
:argument to support it, I pretty much assume that the point is ceded.

No, it just means I'm just getting impatient. :(
 

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