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.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,1e5c102037393131 X-Google-Attributes: gid103376,public From: Richard D Riehle Subject: Re: Assertions Date: 1999/05/21 Message-ID: <7i27tt$hn@dfw-ixnews11.ix.netcom.com> X-Deja-AN: 480325367 References: <3736D243.1EEBF1AB@globalnet.co.uk> <3736F549.E3DDCDEB@pwfl.com> <7h83lc$rd$1@nnrp1.deja.com> <3739CECA.6A49865B@averstar.com> <7hqe7m$q7i@sjx-ixn1.ix.netcom.com> <3742eba6@eeyore.callnetuk.com> <7hv6bb$1l9@dfw-ixnews6.ix.netcom.com> <7i2015$jut$1@nnrp1.deja.com> Organization: Netcom X-NETCOM-Date: Thu May 20 7:04:13 PM CDT 1999 Newsgroups: comp.lang.ada Date: 1999-05-20T19:04:13-05:00 List-Id: In article <7i2015$jut$1@nnrp1.deja.com>, stimuli@my-dejanews.com wrote: >In article <7hv6bb$1l9@dfw-ixnews6.ix.netcom.com>, > Richard D Riehle wrote: > >> The Require, Ensure, and Invariant conditions may be applied to >> a subprogram, a type, or a even some variable. The designer of >> Eiffel (who did not invent these ideas but incorporated them into >> the design of his language), calls this "design by contract." It >> is important to understand that this is a run-time contract. Many >> safety-critical software practitioners feel this is the wrong place >> to evaluate assertions. The SPARK language takes a more conservative >> approach to the same idea. Ada probably needs an approach somewhere >> between SPARK and Eiffel. > >This isn't entirely true, although I think I understand your point. >The Eiffel contract is not a run-time concept, it is a static property >of correct Eiffel systems (read: correct Eiffel programs). I agree that it is possible that some assertions might be checkable at compile time. Most pre-conditions and post-conditions I have seen have not looked like something that could be strictly checked by the compiler -- such things as ensuring that a variable never has a value of zero at run-time. On the other hand, I realize that the Eiffel contract does give the compiler the ability to do conformance checking through assertions and other mechanisms of the contract. This is part of the power of Bertrand's fundamental idea of "design by contract." > It would be correct Eiffel for a compiler >to check the validity of the assertions at compile time and a correct >Eiffel program needn't check them at all. Understood. We agree on this. >Now, given that a general >theorem checker for Eiffel is, in practical terms, very unlikely, >most Eiffel implementations perform runtime checks of the assertions. Yes, this is true. Moreover, we have not yet reached the level of sophistication in software practice where we can apply foolproof theorem checkers on large-scale computer programs. Even Ada does not lend itself to this kind of validity checking. >This is a useful tool for testing and debugging, but it is not the >greater part of what assertions are. My earlier point was that, Assertions, when focused on run-time checking, are not sufficient for safety-critical software development. That is why SPARK put emphasis on assertions that are always evaluated at compile time. Also, it is possible to formulate an assertion that is flawed. Granted, most assertions are simple boolean expressions. Consider, though a post-condition such as, Ensure count = old count + 1 and (P) or (Y and Z) or not P; Someone will find fault with this construct, but I am not interested in absolute correctness of logic at the moment. Most Eiffel developers are careful not to create potentially self-cancelling assertions. There is always someone who will not be so careful. Also, I would not be surprised to see an inherited post-condition in conflict with some new post-condition. Granted, Eiffel has a nice set of features for avoiding this kind of thing, but the discussion concerned implementing assertions in Ada via a pragma. I think it will take a pragma to set the assertions, as suggested, but it might require a pragma to _undefine_ such a pragma to prevent conflicts within a derivation class. The addition of a general assertion mechanism to Ada would please me greatly. I wonder if it is not more complicated than simply adding a few new pragmas. For example, will the assertion pragma on type T be inherited by every derivation in T'Class? This question alone should spawn a whole set of associated questions. In Eiffel this has been thought through carefully. Even so, I not absolutely certain, with my limited knowledge of Eiffel, that one cannot create the kind of errors in Eiffel I suggested in my earlier paragraph. I think this one reason the SPARK devotees are taking such a conservative approach to this subject. I am told this was a concern that prevented a generalized assertion feature from becoming part of the Ada 95 standard. Someone may correct me on this, but I recall a discussion with one of the distinguished reviewers during which I was told as much. I suppose the person with the best perspective on this is Tucker. It would be interesting to hear his view on the why's and wherefore's of excluding pre-, post, and invariant assertions from the Ada 95 standard. Richard Riehle richard@adaworks.com http://www.adaworks.com