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: 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 From: Ted Velkoff Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/08/14 Message-ID: <33F3A389.5080@erols.com>#1/1 X-Deja-AN: 264742755 References: <33E9ADE9.4709@flash.net> <33F133D7.71AC@erols.com> <33F25933.7F83@flash.net> <33F27B5C.6A3C@erols.com> Organization: Erol's Internet Services X-Received-On: 15 Aug 1997 00:29:02 GMT Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-08-14T00:00:00+00:00 List-Id: 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. -- Ted Velkoff