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/08/21 Message-ID: <33FB86CD.92A97B41@munich.netsurf.de>#1/1 X-Deja-AN: 265725293 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> X-Priority: 3 (Normal) Organization: ccn - computer consultant network GmbH Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-08-21T00:00:00+00:00 List-Id: 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?) Regards, Joachim -- Please don't send unsolicited ads.