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: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public From: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/31 Message-ID: <33E0927B.1E45@flash.net> X-Deja-AN: 261211268 References: <33D6451F.4EB@pseserv3.fw.hac.com> <33D7FC7F.141E@flash.net> <33DA36F9.DC446110@munich.netsurf.de> 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-07-31T00:00:00+00:00 List-Id: Joachim Durchholz wrote: > > Ken Garlington wrote: > > What if the mistake is in your code, not the calling code? > > There's always an end to the chain in buck-passing. If the mistake is in > our code, we obviously have to fix it. DBC is not a silver bullet, it is > just a way of unambiguously distributing responsibilities (preconditions > to the caller, postconditions to the callee - and the callee is *not* > required to check its preconditions in its code). > Or, if the system must be fail-safe, the buck is passed up to some > routine that just takes note of the software failure and tries something > else (or detonates the rocked). Or shuts down? My read of the Meyer paper is that DBC is designed to avoid buck-passing: that each routine is essentially bullet-proof internally. However, if the group "distributing the responsibilities" is also the group whose errors you are trying to detect, how does this help? > > > 1. My_Aircraft.Mine is correct. (How is this determined? > > Proofreading. > However, assertions are (hopefully) on a higher level than the program > code, so the task of the proofreader becomes easier by that level. Why would they be expected to be at a "higher level?" Take the example in the Ariane 5 paper. It doesn't appear to have any particular abstration associated with it. Consider also the limits of proofreading described in my draft paper. Furthermore, how does DBC make proofreading any easier than without? > > > Do assertions > > have > > assertions? > > In Eiffel, no. Assertions are on a higher level of reasoning than the > program code itself. The advice is to write simple assertions (again to > make proofreading easier). But writing simple assertions to make it easier to review also implies only writing critical assertions to reduce the workload, doesn't it? And if the wrong critical assertions are chosen, then more errors are likely. > Personally, I'm not totally sure wether this will properly scale up to > arbitrarily large systems. Adding assertions to assertions, however, > adds a second layer of checking (which would have to be read and > understood by the proofreader), so assertions on assertions aren't too > useful anyway. > > > 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. > > This is taken care of. > For single-threaded applications, the problem cannot arise anyway. > For multi-threading, only a single procedure may execute at any time for > a given object. So, in a real-time system, no interrupts can occur while a procedure is executing? How is this managed, particularly for non-maskable interrupts? Assuming it is managed, how can latency be managed in such a system? Is the nulti-threading rule part of the Eiffel spec, or part of an implementation? > > > 4. There are no errors from other sources (e.g. extraneous code, > > higher-tier > > documentation miscommunications). > > You might formalize the higher-tier documentation as deferred (abstract) > Eiffel classes. You might.. if (a) the requirements writer knows Eiffel, (b) all readers know Eiffel, (c) Eiffel has been shown as a useful language for requirements analysis (compare and contrast with tools such as StateMate, for example). > The concrete system is built by deriving from the > deferred classes. DBC makes sure that the concrete classes will abide by > the contracts in the high-level specification classes. > Of course this does not preclude other communication problems. But > there's no silver bullet for this. > > > Also: If the post-condition fails, who provides the corrective action? > > A postcondition failure means the routine is wrong; as it already has > terminated executing, it cannot take corrective action. > So the caller is left to deal with the broken contract - either by > failing its own contract (the default reaction), or by taking corrective > action (catching the exception and trying some other approach). Wouldn't that cause the very Ariane 5 failure that DBC was supposed to prevent? > > > 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)? > > Why > > or > > why not? > > I'm having trouble understanding the situation you're thinking of here. > Usually a class is written by a single programmer/team. Really? Doesn't sound like these routines get reused or maintained over time! > Besides, wether a routine is called once or twice doesn't seem related > to who wrote it, so I'm rather confused here... If different people/teams are each writing a separate piece of code that has an interface between them, then any of the following can happen: 1. One team checks the assertions associated with the interface (e.g. the preconditions are checked by the callee). 2. Both teams do the check, not knowing that the other team is also doing it (or perhaps not caring, if they want their code to be separately reusable.) After all, the callee does make the preconditions available to the caller (see below), so why wouldn't they both end up doing the check (and adding the time to the system). 3. Each team assumes the other team does the check, and neither does it. > > Also: it's my understanding that DBC requires My_Aircraft.Mine be made > > available > > to the client of Assume_Control (no private pre-conditions). Is this > > the > > case > > here? > > Yes. > > > Why or why not? > > The caller must be able to check wether it has fulfilled all > preconditions. It can do so only if all features used in preconditions > are available to him. > > > Does this mean that the pre-condition may be > > checked twice > > before each call? > > Yes. (Only once with precondition checking turned off.) > However, this is misleading. If PBC is in place, you don't have to write > > do_something (My_Aircraft: AIRCRAFT) is > do > if MyAircraft.Mine then > -- do something with My_Aircraft > else > -- declare error > end; > end; -- do_something > > Instead, you write > > do_something (My_Aircraft: AIRCRAFT) is > require My_Aircraft.Mine > do > -- do something with My_Aircraft > end; -- do_something > > which is shorter, and clearly separates the "defensive programming" part > from the really useful code. Not the issue. The caller of do_something (potentially) calls My_Aircraft.Mine, which then calls My_Aircraft.Mine again. This doesn't seem like a particularly efficient way to manage assertions! > > > However, these results seem to be limited to making sure the code does > > what > > you thought it was supposed to do. > > How are the other failure sources > > handled? > > ... > > Also, given that Meyer claims the "most important" effect of > > assertions > > is manual analysis (see section 3.1 of same paper), shouldn't you be > > doing this > > anyway (in addition to any executable testing)? If you're not > > reviewing > > these manually, why not? > > DBC doesn't handle external failure sources. How can this be, if you are "unambiguously distributing responsibilities (preconditions to the caller...". Isn't the caller an "external failure source"? > It is there to make sure > that the code does what it's supposed to do. > As a very useful side effect, it also seduces the programmer into > getting a clear picture of what the routine is actually supposed to do > (something many programmers really need). I would be much more convinced of this if there was a study that demonstrated it. As you note above, excessive assertions can obfuscate as well as clarify, and many Eiffel advocates seem to believe that the more assertions, the better. Isn't this a self-defeating system? > > Regards, > Joachim > -- > Please don't send unsolicited ads.