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: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/08/12 Message-ID: <33F0F6B6.7F83@flash.net> X-Deja-AN: 263810633 References: <33E9ADE9.4709@flash.net> Organization: Flashnet Communications, http://www.flash.net Reply-To: Ken.Garlington@computer.org Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-08-12T00:00:00+00:00 List-Id: Don Harrison wrote: > > 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. Since such decisions are fundamental to the design of real-time systems, isn't this statement equivalent to "it's better to have tool X design my software autonomously than for a human to do it?" I think when you actually start building complex real-time systems, you will see that more locking is not equivalent to better design. > > :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. Very true. In Ada, the "permissiveness" is defined as allowing the programmer to do that which is historically error-prone (e.g. the copy principal). Do you have evidence that enforced blocking on _all_ objects solves a common problem in the design of real-time systems, particularly when excessive blocking often leads to deadlock? > > [...] > > :> :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. Absolutely. In fact, based on some of the discussions, it seems to be reduced almost to a coding standard in some practitioner's mind. (This isn't entirely fair to DBC, of course, but it highlights the problem with calling DBC a "methodology" vs. a "tool" or "technique".) > 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. But all of my requirements are in the documentation! By definition, my code is an _implementation_ of those requirements, not the _definition_ of them. > > [...] > > :> :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. I must have missed it. Could you list the projects again? I saw some hypothetical discussion of why it might scale, but I think Mr. Jezequel is correct: There isn't sufficient _evidence_ to say that it _will_ scale. > > [...] > > :> :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. :( Unfortunate. Having the patience to reconsider the "blindingly obvious" has usually led me to my best work. I find that if I can't put together a logical argument, preferably backed by observable evidence, then I'm probably working on emotion rather than insight. A long time ago, I thought it was "blindingly obvious" that OO approaches wouldn't work in real-time systems. After I started considering the issue further, and doing demonstration projects using OO techniques, I found I was dead wrong. > > > Don. > =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- > Don Harrison donh@syd.csa.com.au