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: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public From: paul.johnson@gecm.com (Paul Johnson) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/17 Message-ID: <5qkla1$4el$1@miranda.gmrc.gecm.com> X-Deja-AN: 257384465 References: <5qi26c$8ll$2@miranda.gmrc.gecm.com> <33CD6207.6007@flash.net> Organization: GEC-Marconi Research Centre Newsgroups: comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-17T00:00:00+00:00 List-Id: In article <33CD6207.6007@flash.net>, kennieg@flash.net says... > >Paul Johnson wrote: >> 1: Eiffel assertions are only executed at certain times, not at every >> invocation of a routine (see E:TL or OOSC2 for the gory details). > >OK, so Eiffel's different. What's the significant advantage of this >approach. The thing to understand about Eiffel assertions is that the mechanism was not thrown together in an ad-hoc manner. The "public" assertions (pre and post conditions, and invariants) are there to support the production of correct classes. A class is "correct" in the Eiffel sense if a client can never see a postcondition or invariant violated, provided that the client follows the preconditions. However if you call a routine from within a class, there is nothing to say that the assertions have to be maintained. In fact it would be very restrictive to say that they must be. What this comes down to is that if I write object.foo (arg1, arg2) then the appropriate assertions should be tested. OTOH if I write foo (arg1, arg2) then the assertions should *not* be tested. >> 2: You can't inherit assertions. Any such system would require lots >> of duplicated assertions. > >Why would I have to duplicate assertions? Because of the Liskov Substitutability Principle. A class must be able to stand in for its ancestors. Therefore it has to inherit the contracts of its ancestors. Therefore when you redefine a routine you need to copy the assertions from the ancestor. Ditto for the invariants. Eiffel does this automatically. >> 3: Invariants are still very tricky to support. You need to call the >> invariant checks at the same time as the pre and post conditions. See >> above for details of when this occurs. >Again, I'm not trying to duplicate Eiffel. How much do I lose if Ada >invariants are different? See above. Remember also that if a routine is not redefined in a descendant, it still has to check the descendant's invariants rather than just the ancestors. You need to define a routine "invariant_check". To add new invariants in a descendant, you redefine this routine to check the new invariant and then call it's ancestor version(s). >> 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. > >Actually, I don't mind the checks being "optimized into oblivion" if the >compiler can deduce that they are unnecessary, 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. >and I certainly don't >want >to exercise one kind of code during development and another during test. The whole point of Eiffel assertions is that in a correct program they have no effect on execution. Therefore you get exactly the same results whether they are enabled or not. Apart from assertion exceptions, the only way that the execution of an assertion can make a difference is if you call a function with side effects. Eiffel functions are specifically banned from having side effects. Of course, you *can* leave them enabled, but it slows down your code. >If Eiffel compilers do no optimizations of assertions, and there are a >lot of complex assertions in Eiffel code, what does this say for the >efficiency of the code? The point of assertions is to detect errors during debugging. Some people leave preconditions on in production code as well, if there are no speed problems as a result. >> [Difficulty of getting "short-flat" forms] >Why would you want to _extract_ such information? The contract is in the >Ada specification in all of my code, at the level of detail I want >public. No its not. The point of software contracting is that the public assertions are just that: public. They are shown in the class interface (the short-flat form). Eiffel takes a different attitude to Ada here, and I can see the case for the Ada approach. Instead of writing interface and implementation in separate files, Eiffel provides tools to extract the interface information from the implementation. The public assertions are part of the interface, because they specify the class behaviour to its clients. The Ada approach has the advantage that you can easily lock the interface while allowing changes to the implementation. In Eiffel this could be achieved by recording the short-flat form of a class (the interface) and checking that the new short-flat form still matches after any change is made. Its just a bit more hassle to organise. Part of the important thing about the short-flat form is that it includes *all* the interface information about a class, including any features inherited from ancestors. This is important, particularly in the presence of multiple inheritance. It means that programmers don't have to search through listings to reconstruct it manually. If you wanted to design a dialect of Ada with software contracting built in properly then you would have to bring the public assertions into the interface file. And you would still need the equivalent of "flat" to bring all the ancestor features into your class. Paul. -- Paul Johnson | GEC-Marconi Ltd is not responsible for my opinions. | +44 1245 242244 +-----------+-----------------------------------------+ Work: | You are lost in a twisty maze of little Home: | standards, all different.