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: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public From: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/08/23 Message-ID: <33FFABE4.2C8E@flash.net>#1/1 X-Deja-AN: 268279626 References: <33E09CD5.634F@flash.net> <33E9ADE9.4709@flash.net> <5siqrr$3of@jupiter.milkyway.org> <5smgts$p68$1@miranda.gmrc.gecm.com> <33EFCCE4.4CE0@flash.net> <5sskfd$nn5$2@miranda.gmrc.gecm.com> <33F25AA5.49ED@flash.net> <5t1fen$c7d$1@miranda.gmrc.gecm.com> <33F52989.38BB@flash.net> <33F83585.2FB006C3@munich.netsurf.de> <33FA76D7.21D9@flash.net> <33FB86CD.92A97B41@munich.netsurf.de> 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-23T00:00:00+00:00 List-Id: Joachim Durchholz wrote: > > Ken Garlington wrote: > > > The issue is that DBC allows to integrate code and code > > documentation > > > better. It is possible to write top-level abstract classes that just > > > encapsulate a few assertions; there is no need to duplicate these > > > assertions in other documents, at Eiffel (at this level) is easy to > > read > > > even for a non-programmer. > > > > To demonstrate the problem, attempt to encode the critical Ariane 5 > > assumption as a "top-level abstract class." It is not directly > > representable > > as code, even as a "top-level" abstraction. > > > > Said another way, could you write "War and Peace" as a "top-level" > > abstraction? > > People keep mixing the documentation aspects and the run-time checking > aspects of Eiffel assertions. > > Assertions as documentation *need not be executable* (so there is no > problem encoding the critical Ariane-5 conditions or even War and Peace > as a precondition). > Assertions for run-time checking must be executable, of course. But even > these double up as documentation on the routine. > > At its first stage, Design by Contract is just a discipline: write down > the preconditions and postconditions of the routine. Make sure the > preconditions and postconditions match what the routine does (easy, the > assertions are in the vicinity anyway). Have them stand out clearly via > keywords so that the "short" tool can create a documentation that > contains the routine signature with their pre- and postconditions. > > The next level is that some assertions may be executable. This allows > run-time checking, and (more important) it encourages the programmer to > actually make assertions and code consistent. Even the non-executable > ones - anybody with some practice in getting the checkable assertions > right will have no trouble putting down precise non-executable > assertions. > > > > > Again: You need to have experience in systems analysis and > > > > requirements > > > > capture to understand that the hard stuff is not readily > > > > expressible in code. > > > > > > Eiffel assertions are *not* code. They are specifications for code. > > > Some of these specifications happen to be checkable at run-time, > > > > Read both of these statements carefully, several times. > > That, coupled with the experiment I describe above, should demonstrate > > the problem with your thinking. > > They don't. Either you don't understand me, or I don't understand you. > (BTW which two statements do you mean?) Simple: You can't have it both ways, You claim that Eiffel assertions are superior because they're executable, while simultaneously claiming they are not executable code. Specifically (quoting you): 1. "Eiffel assertions are *not* code. They are specifications for code." 2. "Some of these specifications happen to be checkable at run-time..." Which ever way you go, you have a downside by your own arguments (executable assertions are limiting; non-executable ones can't be tested during execution). You can't claim the advantages of each without also claiming the disadvantages. It's an interesting dance you're doing, but you will bump into a wall whichever way you jump. > > Regards, > Joachim > -- > Please don't send unsolicited ads.