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.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public From: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/17 Message-ID: <33CEB334.44C5@flash.net> X-Deja-AN: 257536961 References: <5qi26c$8ll$2@miranda.gmrc.gecm.com> <33CD6207.6007@flash.net> <5qkla1$4el$1@miranda.gmrc.gecm.com> Organization: Flashnet Communications, http://www.flash.net Reply-To: kennieg@flash.net Newsgroups: comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-17T00:00:00+00:00 List-Id: Paul Johnson wrote: > > 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. > > 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. OTOH, wouldn't I want the option to see if intra-class dependencies cause assertions to be violated? (Actually, in my case, I generally do want this...) Certainly, if I wanted to have my Ada exceptions raised only from an external caller, it would not be particularly difficult to structure my package to do this. So, other than maybe writing a little less code, what's the significant advantage of this approach? Is it safer to not enforce assertions for intra-class dependencies? I still don't see the big advantage from a safety-critical perspective... > >> 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. To expand: Why do I have to duplicate assertions _in Ada_? > >> 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. Ditto. > >> 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. Since this isn't Ada, I couldn't comment. > > >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. This would require (a) no changes in timing and (b) zero probability that the compiler generates incorrect code with a certain combination of compiler switches and code. I am skeptical. > 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. See above. > Of course, you *can* leave them enabled, but it slows down your code. It does something else. It requires you to decide what to do if the assertion is violated during execution. > >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. What do they do if the assertion is violated? > > >> [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. You haven't read my Ada specs! > 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). Exactly. The Ada specification is just that: the public part. In fact, it's included in our software user's manual for OS-type software for that reason. It defines what the user needs to know, and nothing else. (Actually, we do have to do one thing: we suppress printing of the private part, much like Eiffel uses documentation tools to extract the class specification.) > 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. Right, although I don't the organization as a signficant issue. I would be more worried about making an inadvertant change, and failing to do the check afterwards. Of course, I suspect you could acheive the same effect in Eiffel by having the code in multiple files, and using a CM system to merge the files as needed. > > 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. You can do this in Ada, too, with the proper documentation tools. It's just a bit more of a hassle to organize :) > > 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.