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: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public From: Joachim Durchholz Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/08/20 Message-ID: <33FA3B0F.62780A5C@munich.netsurf.de>#1/1 X-Deja-AN: 268499417 References: <33E9ADE9.4709@flash.net> <33F133D7.71AC@erols.com> <33F25933.7F83@flash.net> <33F27B5C.6A3C@erols.com> <33F3A389.5080@erols.com> 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-20T00:00:00+00:00 List-Id: Matt Austern wrote: > For example, what's the postcondition for a function that sorts a > range? Three postconditions, of course: the range is sorted, the > range has the same number of elements as it did before, and the new > range is a permutation of the old range. (Depending on the sorting > algorithm, you might also have a postcondition that guarantees > stability of equivalent elements.) It's the last one that's a problem; > I never did figure out how to write a postcondition like that in > Eiffel, and I as far as I know it isn't possible. I wouldn't write any of these postconditions in Eiffel; I'd include them in comments. The environment won't check these postconditions for me, true - but I retain the documentation of the routine, at a place where it is easily accessible. > In every language, it's certainly important to document carefully what > a function requires and what it guarantees to do. Eiffel is similar > to all other languages in that many of these requirements and > guarantees have to live in the documentation rather than in the code. Document non-executable stuff in comments. Have your documentation generated automatically. No redundancy, documentation is easy to do along with the formal specs (class interfaces) and/or the coding (routines). Regards, Joachim -- Please don't send unsolicited ads.