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,FREEMAIL_FROM, INVALID_MSGID autolearn=no 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: "Nick Roberts" Subject: Re: Assertions Date: 1999/05/19 Message-ID: <3742eba6@eeyore.callnetuk.com>#1/1 X-Deja-AN: 479683416 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> X-Original-NNTP-Posting-Host: da134d59.dialup.callnetuk.com X-Mimeole: Produced By Microsoft MimeOLE V4.72.3110.3 X-Complaints-To: newsabuse@remarq.com X-Trace: 927132607 02H499TBW8004D443C uk25.supernews.com Organization: RemarQ http://www.remarQ.com Newsgroups: comp.lang.ada Date: 1999-05-19T00:00:00+00:00 List-Id: Richard D Riehle wrote in message <7hqe7m$q7i@sjx-ixn1.ix.netcom.com>... [...] | pragma Pre_condition (boolean_expression [ ... ]); | pragma Post_condition (boolean_expression [ ... ]); What would these actually do that Assert would not? | pragma Invariant (boolean_expression [ ... ]); This construct (I think) could be replaced by an Assert repeated in several places. Would it be so useful as to be worthwhile? (Perhaps it would.) | with the further suggestion that we adopt Require, Ensure, and | Invariant from the Eiffel language. For those of us Eiffel non-cognoscienti, what do these do, please? | One must be careful with assertions as pragmas. It is quite | possible to declare a non-sensical assertion that is never | detected by the compiler. When declaring assertions for a | derivation class, one can construct a boolean expression that | holds for the root of the class but fails for some derived type. 'Twas ever thus. In all cases, the programmer must be as careful to put something sensible into an Assert as into the code proper. Assertions are certainly no panacea: sometimes the code to check up on a piece of code would be more complex to write than the code it's checking; sometimes there is no practical way to check up on it at all; M****y's L*w ensures that bugs can get into the checking code as easily as they can get into the code proper (and be just as much of a S*****g B****r to root out ;-). | This is a fundamental problem with assertions. The more conservative | approach of Ada, in which every type is invariant tends to be more | appropriate for safety-critical software. If there were some way | to formally prove, through a software routine, that an assertion | did not resolve to some completely silly set of propositions during | the derivation process, we might be more inclined to depend on them. | As things stand now, assertion pragmas, while a good idea on the | surface, could easily create more problems than they solve. I would be grateful if you would expand a little on this, perhaps giving an example or two. I apologise to those who don't wish to retread this well-trodden ground, but there some of us who missed the boat first time around, and need to retread it. ------------------------------------- Nick Roberts -------------------------------------