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: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public From: jsa@alexandria.organon.com (Jon S Anthony) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/08/21 Message-ID: #1/1 X-Deja-AN: 265793312 Distribution: world References: <33E9ADE9.4709@flash.net> <33F133D7.71AC@erols.com> <33F25933.7F83@flash.net> <33F27B5C.6A3C@erols.com> <33F3A389.5080@erols.com> <33FA3B0F.62780A5C@munich.netsurf.de> Organization: PSINet Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-08-21T00:00:00+00:00 List-Id: In article <33FA3B0F.62780A5C@munich.netsurf.de> Joachim Durchholz writes: > 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. So, how why write them in such a limited language (either Eiffel or its assertion sublanguage). What's the point? Seems like if this is your stance but you still want some formalism, you should write the things in FOL. > > 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). Sounds OK (note that the non-executable stuff is typically the most important in this sort of context). Of course this is easily done in any language... /Jon -- Jon Anthony OMI, Belmont, MA 02178, 617.484.3383 "Nightmares - Ha! The way my life's been going lately, Who'd notice?" -- Londo Mollari