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: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,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: 257590991 Distribution: world References: <5qi26c$8ll$2@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 bobduff@world.std.com (Robert A Duff) writes: > >> In article , > >> jsa@alexandria.organon.com says... > >> > >> > type Require is boolean range True..True; > >> >... > >> > > >> > Assert : Require := Complex_Precondition(X); > > This isn't quite right, because RM-11.6 allows the check to be > eliminated. Bob, could you clarify this? I just had a look at 11.6 and I'm not clear on how this works. For example given the above it would clearly be the case that you would also have: ... exception when E : Constraint_Error => Do_Something(....)... in order to catch and do something in case the CE is raised. How could the implementation know that this would not "have some effect on the external interactions of the program"???? I don't see how that is possible (but then there's the old saying, "if it happens, it must be possible"...) > >> 4: You had better be pretty sure that the compiler is not going to > >> optimise your checks into oblivion during debugging, and conversely > >> you need a way to turn them off for production code. > > > >??? As long as it is _legal_ (does not change the _meaning_ of the > >code) this would be a _good_ thing! It amounts to verification at > >_compile_ time. > > An optimizer can change the *behavior* of a program without changing its > *semantics*. I know what you mean here, but a more accurate description would be that an optimizer can change the behavior as long as that behavior is not part of the defined semantics. > This is true in all programming languages, including Ada. Mostly, > you're right -- if the optimizer can prove an assertion at compile > time (and the optimizer is not buggy) then that's good. But the > 11.6 cases I mentioned above are troublesome. In Ada, I prefer to > use an Assert routine, or a pragma Assert (if supported by the > compiler). End users care about the *behavior*. Actually, if they really did care about behavior that was _not_ part of the defined semantics, wouldn't that really be a case of an "erroneous" or possibly "bounded error" program???? /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