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: 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 X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public From: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/23 Message-ID: <33D6A2EE.325@flash.net> X-Deja-AN: 258637939 References: <33D43D93.6A8E@flash.net> Organization: Flashnet Communications, http://www.flash.net Reply-To: kennieg@flash.net Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-23T00:00:00+00:00 List-Id: Don Harrison wrote: > > Ken Garlington wrote: > > :Don Harrison wrote: > :> > :> First, part of the reason it looks complicated is that it is only emulating > :> (in Ada83) the real thing. As I've already said, I wouldn't implement assertions > :> this way if I had the proper tools to work with. If you express it in Eiffel, > :> it becomes simpler. > : > :OK - could you post the Ada equivalent? > > Sure. Assuming the availability of a postcondition clause, > > type Input_State_Type is (.., Menu, ..); > > Input_State : Input_State_Type; > No_of_Keys : Natural > Menu_Option_Selected : Boolean; > Submenu_Option_Selected : Boolean; > > ... > > function in_menu_state return Boolean is > begin > return (Input_State = Menu and then No_of_Keys = 0 and then > not Menu_Option_Selected and then not Submenu_Option_Selected); > end; > > procedure Interpret_CLR_Key is > begin > ... > ensure in_menu_state -- General assertion > end; > > Note that there is no precondition on Interpret_CLR_Key in accordance with the > fact that the Console Operator should be able to press any key at any time > without having the software fall over. Using assertions to validate input > would be a misuse of DBC. Compare this to the Ada code you presented earlier. Why is this significantly simpler or easier to read? > > :> Second, the compound condition represents a single higher level condition > :> which can be declared as a function. > : > :But doesn't that just postpone the complexity? Making the assertion > :nearest > :the point the reviewer is reading less clear, and requiring a search > :through > :other files to discover the meaning of the higher-level condition? > > Yes, but this is no different from using encapsulation for abstraction anywhere > else to simplify. You aren't going to replace every call in a procedure > with the actual code of the called procedures (a compiler may, but a human > shouldn't). Neither should you do this for assertions. You don't suddenly forget > about abstraction just because you're writing an assertion. True, but remember that we are asking a human reader to not just understand what is required from a user's point of view (where abstraction permits unncessary details to be hidden), but to verify if the software will function correctly or not. Doesn't this imply that the evaluator will likely have to understand more than that required by a user of the interface? > A prerequisite for (any kind of) abstraction to be effective, of course, is > meaningful identifiers. If your identifier names accurately reflect what you're > trying to model, a high-level assertion immediately makes sense and you only > look further if you really need to know the details. This would be the case, > for example, if investigating the cause of an assertion violation or conducting > a manual code review. Exactly my point. Meyer claims that such manual reviews are the primary benefit of assertions. However, abstration does not necessarily assist such a review; in fact, it may complicate it. > Otherwise, the higher-level abstraction is not only > sufficient but desirable (unless you want to be needlessly swamped by compexity). > > Using meaningful identifiers sure makes a big difference to intelligibility and, > IMO, is a skill that can be acquired by any reasonably literate developer > who is suitably encouraged (read "forced" to use them). However, if the intent is to discover errors made by the developer, to what extent can the reviewer trust those "meaningful identifiers"? > :For that matter, if this is the correct method, why not do it in Ada? > > Purely historical reasons. If the code wasn't frozen at the moment, I probably > would. Then this doesn't seem to be an advantage of Eiffel over Ada, as your earlier comment indicated. > > :>: Wouldn't it be just as easy to say, in the description of this > :>: operation, the > :>: English text preceding it? > :> > :> ..and lose the benefit of being able to execute it? > : > :According to Meyer, the principle benefit is the documentation value. > > I don't know whether he said this, but I'm not sure that I agree. I'll only > find out through experience.. See section 3.1 of my analysis of his Ariane paper, at: http://www.progsoc.uts.edu.au/~geldridg/eiffel/ariane/ > :As to execution (either during test or operation), see sections 3.2 and > :3.3 of > : > : http://www.progsoc.uts.edu.au/~geldridg/eiffel/ariane/ > > This is irrelevant to what we are dicussing here - use of DBC in non-HRT > situations. It should be quite plain by now that I agree with you about the > dangers of using assertions in HRT threads using current technology. > > :> :... So, unless you propose teaching DBC > :> :to all engineers in the program (which might not be a bad idea, > :> :actually), > :> > :> I agree, it would. > : > :But unlikely, unfortunately, given the history of such attempts. > > Quite true. > > :> I don't know what ADARTS is but it's one thing to be told you have to think > :> of all assumptions and another to demonstrate you have as evidenced by coded > :> assertions. > : > :Again, from a documentation standpoint, why is writing code better than > :documenting the assertions in a form the reviewer understands? > > Consider the aversion of developers to documenting code. It's viewed by them > as a necessary burden which doesn't actually make the software work so there's > little motivation to do it. Executable assertions, OTOH, actually contribute > something (runtime checks) to a running program. Therefore, they have some > material value in the mind of a developer and their more likely to use them. I'm not sure I agree that well-trained and professional developers feel this way, but let's say they do. Wouldn't this imply that they will be biased toward adding code that helps them get their code correct for the current use of their code (i.e. that part that provides direct value to them) and much less attention to addressing issues that don't provide value to them (e.g., handling errors due to improper reuse by "some other guy")? > The by-product is that the code gets documented for free and the developers > actually *want* to do it. It also seems that the documentation value of the assertions will be lessened (less likely to use meaningful identifiers vs. ones that "work good enough"). The line between codes that don't like to write documentation vs. coders that don't like to write self-documenting code for others to read appears to me to be easy to cross... > > :> :I also challenge whether or not you code all of the assertions you can > :> :envision. > :> :Look at your example from earlier. There's absolutely no other > :> :assertions you > :> :could consider? > :> > :> There may be others but so what? The existence of any I may not have thought > :> of doesn't negate the effectiveness of those I *have* thought of. > : > :But how do you draw the line between the assumptions you state and the > :assumptions you leave silent? > > Sorry, not sure what you're driving at. Every error condition that might occur (e.g., adding extra code that makes an extraneous assignment), but is not checked by an assertion, would appear to be an undocumented assumption. Every undocumented assumption, per Meyer, represents an incomplete description of the interface. How do you decide which assumptions not to document? > :And what does that do to the oft-said statement that Eiffel programmers > :put in assertions for unlikely events? > > That's what all (or at least most) assertions are. They're catering for the > unlikely event that the developer has made a logic error. Most of the time > we write code with correct logic but occasionally we make mistakes. These > mistakes can often be picked up by an assertion. So, how are the likely events detected? And, if the same person who made the logic error writes the assertions, why is it reasonable to expect that the assertion detects the error? Won't the person simply make the same mistake in logic, particularly for such things as missed requirements? > :> :How about the possibility that calling one of the > :> :functions > :> :in the assertion causes NO_OF_KEYS to become non-zero, just for fun? > :> > :> As I don't write functions with side effects, I'm not sure why I would want to > :> do that!.. > : > :More correctly stated, you don't _intend_ to write assumptions with side > :effects, so you _assume_ there's no need to write an assertion to > :confirm > :that you, in fact, met your intent. > > You mean meta-assertions? Obviously, Your question in tongue-in-cheek but > does highlight the fact that there is practical limit beyond which you don't > want to go and meta-assertions are well beyond that limit. Most people want to > go home at the end of the day. I don't know why this is a "meta-assertion." Extraneous code is a category of error, just like missing code. Given that "most people want to go home at the end of the day," my point stands. Which assumptions do you document? Which do you remain undocumented? And what theory drives the decision? Does DBC say, "this type of coding error is more likely than the other, so protect against it first?" > :How do you catch software design faults in your code if you assume you > :made > :no mistakes in your code? > > Don't follow. In writing assertions, you assume you *will* make design mistakes > in the code proper. Except that you deliberately exclude classes of faults, apparently, without any statement in the code that you did so. > If you're talking about design faults in assertions, I've > already answered you previously - the code proper acts as a built-in assertion > validation mechanism. Think again, particularly with respect to missing code. > > :> Documented contracts are a good idea and may be appropriate for your domain. > :> Their weakness is that they can't be enforced, so for *other* domains, I would > :> prefer executable assertions. > : > :A perfectly reasonable approach, for those domains that (a) can live > :with > :executable assertions and (b) where the documentation effect is best > :expressed in code. > > Agree. > > :> There already was one, but it would be better to also have a higher level > :> one for initialisation. This would aid testing in that if you fed in the > :> wrong profile, you could verify that the IRS will not work. It wouldn't rely > :> on the more obscure low-level assertion that was actually violated. > :> > :> In IRS: > :> > :> set_operational_profile (profile: OPERATIONAL_PROFILE) is > :> require profile_compatible (profile) > :> do .. end > : > :This would require that the profile be stored in memory, wouldn't it? > :The profile is a textual/graphical description of the behavior of the > :environment. > > No, it simply requires that the thing you want to make assertions about can > be abstracted in some way. This implies both attributes (data) and operations > on those attributes. If you can abstract a profile using a class (which I'm > sure you could), then you can make assertions about it's compatibility. Don't assertions involving the enviroment require data about the environment? > > :You might be able to express it as "The horizontal acceleration shall > :not exceed xxx..." ... and in fact, it probably would make more sense > :to express it exactly that way (in English!) so that it is clear at > :the requirements level. > > You can do both. I'm not sure I agree with the claim that all comments can be written as code! > > The other examples actually aren't applicable to the efficacy of DBC as > they stem from errors in specification documents.. WUPS! DBC doesn't protect against errors in specification documents? An interesting statement! Given this, then it shouldn't be able to protect against misinterpretations of specification documents by a developer, either, true? Or, for that matter, misinterpretations of any higher-tier document (e.g. a design document)? Doesn't a requirement not read equate to a requirement not written? Finally, of all of the errors in code, assuming the use of existing techniques (code reviews, unit test, etc.) how many are "code-only" errors vs. misinterpretations of higher-tier documents? > > Don. > =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- > Don Harrison donh@syd.csa.com.au