From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: fac41,2c6139ce13be9980
X-Google-Attributes: gidfac41,public
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
X-Google-Thread: f43e6,2c6139ce13be9980
X-Google-Attributes: gidf43e6,public
X-Google-Thread: 1108a1,2c6139ce13be9980
X-Google-Attributes: gid1108a1,public
From: Ken Garlington <kennieg@flash.net>
Subject: Re: Safety-critical development in Ada and Eiffel
Date: 1997/08/07
Message-ID: <33E9ADE9.4709@flash.net>
X-Deja-AN: 262817044
References: <33E09CD5.634F@flash.net> <EEJ4B7.40p@syd.csa.com.au>
Reply-To: kennieg@flash.net
Organization: Flashnet Communications, http://www.flash.net
Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel
Date: 1997-08-07T00:00:00+00:00
List-Id: <comp.lang.ada>


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

> 
> :> :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, but other methodologies do discuss error recovery techniques, and
how to
apply them. This is particularly important if the error won't be
uncovered
until after it is delivered.

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

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.

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

Which is completely contradicted by the abve statements of using
assertions
for execution purposes.

The whole point of a methodology is to guide the thinking of an analyst.
It
doesn't sound like DBC/Eiffel has given you much in the way of guidance.

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

More to the point, you haven't given any evidence that DBC/Eiffel has
any
particular advantage in this area.

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

Has such automated optimization been done in practice? Isn't such an
optimization
on the same difficulty level as the toolset automatically generating the
correct assertions for each interface?

> 
> :> (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), can
requeue
requests, etc. More choices for the designer usually means additional
flexibility, I would think.

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

But you gain flexibility in their timing capabilities (which is what we
were
discussing, remember? :). Given that the purpose of a protected type is
to
define time-based aspects the system, isn't this the more valuiable
flexibility
for this type of object?

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

You said that you did not provide exhaustive coverage via assertions. If
that
doesn't mean that you assume the condition will not occur, what does it
mean?
That you assume it will occur, but do not address it?

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

Then what does it matter what a "runtime error checking mechanism" does?
The question remains: How does DBC address documentation-related
problems?

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

Given that, then if DBC does not address this area, it must be
deficient.

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

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

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

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

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