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: 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: paul.johnson@gecm.com (Paul Johnson) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/18 Message-ID: <5qnab3$ft$3@miranda.gmrc.gecm.com> X-Deja-AN: 257569291 References: <5qi26c$8ll$2@miranda.gmrc.gecm.com> <33CD6207.6007@flash.net> <5qkla1$4el$1@miranda.gmrc.gecm.com> <33CEB334.44C5@flash.net> Organization: GEC-Marconi Research Centre Newsgroups: comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-18T00:00:00+00:00 List-Id: In article <33CEB334.44C5@flash.net>, kennieg@flash.net says... > >Paul Johnson wrote: >> 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...) You can always put in "private" assertions, such as "check" clauses (similar to the classic C "assert" macro), and loop variant and invariant clauses. >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. How? It sounds like you would have to have internal and external versions of all routines, all suitably redefined in the presence of inheritance. This is not a trivial suggestion. >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? Suppose I have an invariant in my class: "foo (a, b) = 0" This states a relationship between a and b. Now my class could have one routine which computes both a and b simultaniously. Or it could have one routine which computes a, and another routine which computes b. This is purely an internal implementation decision, so I should be able to chose either. But if I have in my class the following two lines compute_a; compute_b; then under your scheme I will get an exception. As "compute_a" terminates, the invariant will be checked, and will fail. So the public assertion constrains the private implementation. (Actually, its even worse. If I assign to a and then call any routine before assigning to b then I'll trip the invariant check) >I still don't see the big advantage from a safety-critical >perspective... The Eiffel rules for assertion checking allow the software to be laid out in the most logical manner, making proper use of functions and procedures. This helps the programmers avoid bugs. >> >Why would I have to duplicate assertions? >> >> Because of the Liskov Substitutability Principle. > >To expand: Why do I have to duplicate assertions _in Ada_? Well, Ada these days has inheritance. If you want to write correct software then descendants must inherit their ancestors contracts. If you want to check and document this then you have to write the appropriate assertions. >> 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 ...". Of course there are other ways of writing assertion checks in Ada. >> 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 If your software depends upon timing for the correctness of its results then I would certainly not want to see your software used in safety critical applications. I agree that timing variations can cause different results, but why would they cause incorrect results? If they don't cause incorrect results then why are you worried? >and (b) zero probability >that the compiler generates incorrect code with a certain combination of >compiler switches and code. I am skeptical. What does this have to do with the problem under discussion? I agree that this can happen, but why does the ability to enable and disable assertions cause any new problems? >> 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. 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. Sometimes a function will cache a result for future use. I've written table classes that do this. Such functions are fairly rare. When detected by static checks they can either be inspected carefully or simply banned. >> 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. Surely the same arguments apply to Ada? Look at Arianne 5. >> 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? Depends on the application. Generally they print an error report, dump stack information to a file, and ask the user to phone the vendor. Note that I am not proposing this for real-time embedded applications. However there are safety-critical applications which are not real-time. >> >> [Difficulty of getting "short-flat" forms] >You haven't read my Ada specs! Are you saying that you write the contract in comments in the spec? If so then good for you: its good practice. The problem is that you have now duplicated the information: one copy is in comments, and the other is in the assertions in the code. Hence you have doubled the associated work, and increased the risk of an error. Eiffel requires that you write the contract once, and uses the text for both purposes. I'll agree that all of the benefits of Eiffel assertions are available in Ada if you put in enough work, but why all this effort to do something that Eiffel does automatically? Also if the work becomes too onerous then it tends to get dropped when schedule and budget pressure is on. This has been the vice of software engineering ever since the discipline was invented. Eiffel makes good practice so cheap, easy and obvious that people do it without needing to make a special point of it. [Stuff about deriving documentation from specs deleted: we seem to be in broad agreement] 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.