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=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC 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 X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public From: warwickp@syd.csa.com.au (Warwick Pulley) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/17 Message-ID: #1/1 X-Deja-AN: 257335198 Sender: news@syd.csa.com.au X-Nntp-Posting-Host: dev2 References: <33CD1722.2D24@calfp.co.uk> Organization: CSC Australia Pty. Ltd. Reply-To: warwickp@syd.csa.com.au Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-17T00:00:00+00:00 List-Id: In article <33CD1722.2D24@calfp.co.uk>, Nick Leaton writes: > Warwick Pulley wrote: > > > I have seen this happen at least once, where an executable was released to > > the test group which AFAIK was only tested with assertions enabled, and then > > it was discovered that a crucial line of code was removed because it was > > within an assertion block and once this error was encountered the executable > > didn't crash but its functionality was imparired severely enough so that > > it had to be run again. > > Can you explain this a bit more. In Eiffel an assertion has to be > a boolean expression, and I presume that you are not writing a > boolean expression that has a side effect? Personally I haven't used assertions to their full extent although I like to have error checking in place. It turned out that the problem lay not in the boolean expression itself, but how it was used. The example I was referring to above, which was also modelled in Ada, was not of the form: -- example 1 if and then not then raise end if; return but looked like: -- example 2 if and then then return end if; raise ; This of course worked fine when assertions were on because when the check was satisfied a value was returned and the assertion was avoided. When assertions were switched off and the procedure got called, an exception was raised unconditionally and broke the software during testing. I my last post I mentioned a method of using assertions in Ada to address this problem, namely by using *one-line* calls to inline precondition and postcondition checking procedures. They also had the advantage that the assertions could be included only when a compiler directive was set to TRUE, rather than using a boolean statement. When assertions were off, the body of the procedure would be a "null;" statement which would get optimised out. I hope. :) Example 2 above is an example how the assertions can be "mis-implemented" in Ada, because the logic is wrong and necessary code was included in the "if" statement. As you have said, all you need in Eiffel is the boolean expression itself, and since Eiffel has a special clauses for these assertions it's not possible to include vital procedural code within these clauses. Although I made the point about Ada specifically, I then made it unnecessary by making the broader statement that I would be uneasy about releasing software that was untested with assertions removed. This would be whether the language I program in supports assertions or not, and I guess the same goes for any software that's released in a different form to which it is tested. > -- > > Nick Regards, Warwick.