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: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: jsa@alexandria.organon.com (Jon S Anthony) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/18 Message-ID: #1/1 X-Deja-AN: 257628592 Distribution: world References: <5qi26c$8ll$2@miranda.gmrc.gecm.com> <33CD6207.6007@flash.net> <5qkla1$4el$1@miranda.gmrc.gecm.com> <33CEB334.44C5@flash.net> <5qnab3$ft$3@miranda.gmrc.gecm.com> Organization: PSINet Newsgroups: comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-18T00:00:00+00:00 List-Id: In article <5qnab3$ft$3@miranda.gmrc.gecm.com> paul.johnson@gecm.com (Paul Johnson) writes: >>> In many compilers, if you say "assert: require = (a > b)" then the compiler >>> will observe that the value of "require" is not used thereafter, and >>> remove the statement. >> > >Since this isn't Ada, I couldn't comment. > > This discussion started when someone (I assumed it was you, sorry I > didn't check) proposed a type "require" defined as a subrange of > Boolean constrained to be true. The above statement declares a > variable "assert" of type "require" and initialises it to "(a > b)". > If this expression evaluates to false then a range exception will be > triggered. Sorry if I've got the syntax wrong, and sorry that my > explanation was wrong as well: I should have said "... the value of > 'assert' is not used thereafter ...". Actually, that would be myself who posted that (well known) idiom. Please note that any compiler that did what you suggest without static versions of a and b would be buggy. If a and b are computed or passed in or whatever, the only way that the compiler could blow off the code would be if it did complete inter-procedural analysis to ensure that no side effects anywhere could _possibly_ occur in the computation of a and b. Of course, if it could do that and still infer what the assert would be, then of course it would be free to insert a Constraint_Error in place of the code (if it was determinted to be false) or simply remove the code (if it was determined to be true). But in general, your scenario is either fantasy or a bug in the compiler. > Functions that might have side effects are fairly easy to detect (they > assign to non-local variables, or call other routines that do so). This > can be statically checked. Yes, this is "possible", but in the general case, basically impractical. The call graph could be extremely large and complicated - especially in a dispatching environment. Even worse - you can add to the call graph in an inheritance based extension without going back and recompiling everything that _might_ end up calling your new side-effect inducing function. That's actually part of the point of such OO style extension. In fact, you might not even be _able_ to go back and recompile everything even if you decided to take that stance. Any library code that a client might extend, for which there is no available source will be impossible in principle to fix up in this way. In short, this is easier said than done and your comment evinces a rather naive view of the matter. In Ada you can "tag" such a function as having no side effects by placing it in a "Pure" unit. But even in this much more restricted setting it is hard to give absolute guarantees. > >It does something else. It requires you to decide what to do if the > >assertion is violated during execution. > > Surely the same arguments apply to Ada? Look at Arianne 5. This is completely irrelevant to the Ariane 5 case. I'm not sure why people can't seem to twig this fact. /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