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.2 required=5.0 tests=BAYES_00,INVALID_MSGID, 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/24 Message-ID: <33D7FC7F.141E@flash.net>#1/1 X-Deja-AN: 258803574 References: <33D6451F.4EB@pseserv3.fw.hac.com> Organization: Flashnet Communications, http://www.flash.net Reply-To: kennieg@flash.net Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-24T00:00:00+00:00 List-Id: 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, how do they know what corrective action they should take? If the erroneous code is reused in another application, doesn't it carry its error along with it? What if the mistake is in your code, not the calling code? > 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? Do assertions have assertions? What happens if an assertion's assertion fails, and how is it distinguished from an assertion failure?) 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. 4. There are no errors from other sources (e.g. extraneous code, higher-tier documentation miscommunications). Correct? Also: If the post-condition fails, who provides the corrective action? 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? 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? Why or why not? Does this mean that the pre-condition may be checked twice before each call? > We now move on to the next > component and repeat the process. Step-by-step, piece-by-piece we construct > our reliable ATC system. We did so *incrementally* through a divide-and-conquer > strategy and by being demanding in what we expected of callers and demanding > of ourselves in producing the correct results. 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? > Sorry if this is a bit Mickey Mouse for some, but some may find this helpful. > > [the "doing so" following means checking the validity of all calls] > > :In safety-critical > :software, how can you justify not doing so? > > If timing is so desperate that you can't use assertions, you may *have* to > do perform this sort of analysis manually. I think timing is part of the issue, but there are certainly other issues. See sections 3.1.6, 3.2.2, and 3.3 of my draft paper at: http://www.progsoc.uts.edu.au/~geldridg/eiffel/ariane/ 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? > > Don. > =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- > Don Harrison donh@syd.csa.com.au