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: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public From: Matt Austern Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/08/18 Message-ID: #1/1 X-Deja-AN: 265738128 References: <33E9ADE9.4709@flash.net> <33F133D7.71AC@erols.com> <33F25933.7F83@flash.net> <33F27B5C.6A3C@erols.com> <33F3A389.5080@erols.com> Organization: SGI Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-08-18T00:00:00+00:00 List-Id: Ted Velkoff writes: > Matt Austern wrote: > > > > Have preconditions and postconditions been extended in recent versions > > of Eiffel? I haven't yet read the second editon of Eiffel: The > > Language yet, and I haven't used Eiffel for a year or so. When I last > > did, though, there were a number of restrictions on them. I note > > that, because of those restrictions, many of the interesting > > preconditions and postconditions in ETL itself were written as > > comments rather than as executable code. > > You are correct that there are (still) limitations to the expressiveness > of assertions. In particular, one cannot write executable quantified > expressions, e.g. "for_all x in y it_holds x.item > 0". This would be a > valuable capability indeed, since one could, for instance, compile > (that is, type check) an analysis or design, including its assertions. > > In my view, the fact that some kinds of assertions are not executable > does not lesson the value of Eiffel. I would hazard a guess that at > least 75% to 80% of the assertions one would want to write are of the > form that are supported. For me, that is still a big gain. That hasn't been my experience: my experience, when I did use Eiffel, was that most of the interesting preconditions, postconditions, and invariants tended to be complicated enough that I couldn't express them within the language itself. 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. 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.