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=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID 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: Joachim Durchholz Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/26 Message-ID: <33DA36F9.DC446110@munich.netsurf.de>#1/1 X-Deja-AN: 259327101 References: <33D6451F.4EB@pseserv3.fw.hac.com> <33D7FC7F.141E@flash.net> X-Priority: 3 (Normal) Organization: ccn - computer consultant network GmbH Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-26T00:00:00+00:00 List-Id: 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). > 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. > 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). 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. > 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. 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). > 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. Besides, wether a routine is called once or twice doesn't seem related to who wrote it, so I'm rather confused here... > 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. > 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. 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). Regards, Joachim -- Please don't send unsolicited ads.