Re: Safety-critical development in Ada and Eiffel

[jtc@jupiter.milkyway.org (Jim Cochrane)]

In article <33E9ADE9.4709@flash.net>,
Ken Garlington  <kennieg@flash.net> wrote:
>Don Harrison wrote:
>> 
>> 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. :)
>
>Eiffel advocates need to decide: Is the primary value of assertions for
>documentation
>(as Meyer maintains) or to raise errors during execution (which has a
>number of
>drawbacks, including potentially postponing the detection of the problem
>until well
>after it is delivered).

I think the most important use of Eiffel assertions (specifically
require, ensure, and (class) invariant) is for documentation - that is,
to provide a precise specification of the precondition and postcondition
for each public method and of the class invariant.  Specifications that
are not codable can still be documented as comments.  Tools that are part
of the standard Eiffel environment automatically extract these specifications
so that a programmer who is using a class will have access to the
documentation of the class's interface without needing to look at the
class implementation.

> ...
>> 
>> :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. For example:
>
>1. How, specifically, does DBC support error detection prior to
>execution?
>(Not writing down potential error sources, but actually determining if
>the
>error exists in the particular application.)

The concept of design by contract is simply an extension of the ideas
presented by Dijkstra, Gries, and others on the design of correct
programs.  An important component of these ideas is the specification of a
precise pre- and post-condition for each coded procedure.  The extensions
made to this component by the principle of design by contract include
adapting it to an object-oriented system (by adding class invariants
and having the procedures belong to a class) and providing language
support for these specifications.

To address the above question in this context, design by contract can
be used as part of a formal development process that uses design and
code inspections as a means of detecting and removing design and code
defects.  The technique of precisely specifying class interfaces,
aided with tools to extract this specification to make it easily
available, enhances the inspection process by making these interfaces
explicit.  Thus, for example, when the implementation of a method m that
uses class X is inspected, the use of X's methods by m can be examined
to determine if m uses X's methods correctly; this is done by checking,
for example, for a call of X.a in m, that the precondition of X.a will
be true when the call is made.  Additionally, m's postcondition can
be used during an inspection to check if it will always be true by
analyzing the implementation of m - that is, by answering the question:
When m's implementation is executed, will it always terminate with
the postcondition true?

Thus (in my opinion), design by contract is not a method.  Rather it
is a technique that is a useful component of a method.  The contribution
of the this technique is that it ensures a precise and explicit
specification of a class interface so that the use of the interface
can be examined by means of its pre-conditions to make sure that it
is used correctly, and the implementation of the interface can be
examined by means of its post-conditions and class invariant to make
sure that it is implemented correctly.  In any object-oriented design,
all class interfaces will have specifications.  If the specifications
are not explicitly documented, it will be more difficult to use the
interface correctly.  When the specifications are explicitly documented,
it becomes easier to use the interface correctly, as well as easier to
detect defects in the use or implementation of the interface.

>
>2. By extension, how does DBC support error detection after reuse?

If I understand what you're asking, design by contract can be used to
detect errors in the use of a reusable component by examining the
use of the component by the client code and determining if the
pre-conditions specified by the reusable component's interface are
true for every call in the client code of a method belonging to the
interface.

>
>3. For those errors not discovered (which will presumably cause run-time
>exceptions), how does DBC guide the designer to handle these exceptions
>(which were not expected to occur)?

I think that the originator of the concept of design by contract,
Meyer, has presented some guidelines for handling exceptions.  However,
although these guidelines may be helpful, I think the designer of
the software is going to need to decide how to handle each situation
where an exception could occur.

>
>4. How does DBC help detect inconsistencies between code and
>requirements,
>or for that matter internal consistencies within the requirements?

Again, (in my opinion) design by contract is not a method; and it cannot
solve these problems.  It should be used as part of a method.  Areas
such as these that are not addressed by design by contract, should
be addressed by means of other method components.  Design by contract
could help to detect inconsistencies between code and requirements,
since it makes the interface specifications of the code explicit, thus
making it easier to detect such inconsistencies simply because the
documentation of the specifications is available; but it cannot be
used as the only means to detect these inconsistencies.

From your post, my impression is that you are assuming that design
by contract is a method whose purpose is to develop software as free
from defects as possible.  I think if you adjust your view and look
at it as a technique or tool that is part of such a method, this may
clear up some of the confusion.  In other words, the application of
design by contract will not guarantee high quality software.  This is
only possible if it is applied wisely as part of a comprehensive method.
And even a comprehensive method cannot guarantee high quality software;
it is also necessary to apply one's own exertion, intelligence, and
wisdom.  A method may guide us in developing high quality software,
but we will still need to make difficult decisions.  Regardless of the
method used, a poorly made decision can detract from the quality of the
software we are developing.


Jim Cochrane
jtc@dimensional.com

>
>Given that we both agree (as noted earlier in the post) that the key is
>for the designer to think, how does a coding convention support such
>thinking - not in terms of general OO concepts like polymorphism and
>inheritance (which other languages, including Ada, have) but in terms of
>error detection and correction?
>
>> 
>> :> :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.
>
>Wait a minute! Here's the possible scenarios:
>
>1. The post-condition fails during initial development. In this case,
>the
>developer of the code fixes the problem (or changes the post-condition,
>as unfortunately sometimes happens). However, how often is the
>post-condition
>going to fail at this point? The developer writes both the code and the
>post-condition, so it's likely that they will match at that point.
>
>2. The post-condition fails after delivery. The developer may no longer
>be around
>to fix the problem. Furthermore, if there is a rescue clause, what does
>it do?
>What guidance does DBC provide.
>
>3. The post-condition fails during reuse development. Same outcome as
>#2. This
>is the most likely case for a post-condition failing - where the
>environment
>in which the module is used changes.
>
>Any methodology that postpones finding errors until the code is reused
>is going
>to be difficult to sell as "reuse-friendly".
>
>> 
>> 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.
>
>Hasn't this whole discussion been in terms of how to detect errors in
>the code?
>Isn't it a little naive to assume that the code will be written
>correctly as a
>precondition for finding errors in the code?
>
>For that matter, if it's the client's responsibility, and it doesn't
>hurt if
>the assertion is not performed by the object being used, then doesn't
>this
>cut the legs out of an argument of Eiffel's power? Pretty much any
>language
>can provide assertions for the client to manually call prior to using an
>operation.
>
>> 
>> 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.
>
>You're assuming a lot about automated optimizations across object
>interface
>boundaries. Is there evidence that Eiffel compilers do such
>optimizations
>successfully? Worse, you're again in the "proof by execution" mode. What
>does
>this extra code do in terms of readability, for example?
>
>> :If both teams do the call, this is not nice from a
>> :efficiency standpoint.
>> 
>> See above.
>
>Ditto. Any methodology that says, "Write as much code as you want, the
>compiler will optimize it" doesn't seem to be a strong methodology, in
>my opinion.
>
>> 
>> :> 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.
>
>We'll just have to agree to disagree on this one. Again, I would rather
>have a methodology that helps me think about the issues vs. coding them.
>
>> 
>> :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."
>
>Please summarize your arguments/evidence that DBC helps find
>documentation-
>related problems.
>
>> 
>> :it has limitations with respect to implementation language,
>> 
>> More accurate is to say that most languages provide limited support for it.
>
>Two responses:
>
>1. I was discussing limitations in Eiffel, and
>
>2. Other Eiffel experts disagree with you with regard to other
>languages:
>
>See the post on Internet newsgroup comp.lang.eiffel "Re: Papers on the
>Ariane-5
>crash and Design by Contract," Jean-Marc Jezequel, 1997/03/18: "Ada's
>subtype
>declarations are a kind of contract, that could be documented as such.
>Design
>by contract is not specific to Eiffel. You can do it with any language,
>just
>because it is a way of designing!"
>
>> 
>> :it's not clear that it scales well,
>> 
>> Not true.
>
>Can you provide evidence to the contrary?
>
>See Internet newsgroup comp.lang.eiffel post "Re: Papers on the
>Ariane-5 crash and Design by Contract," Jean-Marc Jezequel,
>1997/03/18: "...at least in the case of Ariane 501, simple assertions
>(a la Eiffel and other languages) would have been expressive enough to
>specify the fatal hidden assumption. Whether the last point scales up
>to a full sized mission critical system is still an open question.
>I'm quite confident it is so, but I've only my own experience with telco
>systems to back it up."
>
>> 
>> :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.
>
>But interface errors, by definition, are not localized. They are
>generated
>due to the interaction between objects (in some cases, a long thread of
>object interactions). The Ariane 5 case is a perfect example of this.
>
>Requirements/design mismatches, similarly, are not localized since the
>requirements are usually not written in terms of objects. One of the
>designer's jobs is to map the requirements to objects. Even for
>requirements that are object-oriented, they are usually a much higher
>level than the implementation.
>
>Again, you're thinking of run-time error detection. This is the worst
>place
>to detect errors. Consider, for example, the errors made in the Eiffel
>implementation of the scaling routine presented in their Ariane paper.
>If these errors were "blindingly obvious", why did it take a year for
>anyone to say anything about them?
>
>> 
>> :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.
>I will say that if error recovery is blindingly obvious, then there's
>a lot of work in the fault tolerance world that's apparently just a
>waste of money. :)
>
>> 
>> All of these points have been made before.
>
>Unfortunately, I think you're right. It doesn't seem as though we're
>communicating very effectively. I'll concede the argument to you.
>
>> 
>> Don.
>> =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
>> Don Harrison             donh@syd.csa.com.au