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: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public From: donh@syd.csa.com.au (Don Harrison) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/23 Message-ID: X-Deja-AN: 258251019 Sender: news@syd.csa.com.au X-Nntp-Posting-Host: dev50 References: <33D43D93.6A8E@flash.net> Organization: CSC Australia, Sydney Reply-To: donh@syd.csa.com.au Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-23T00:00:00+00:00 List-Id: 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. :> 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. 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. 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). :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. :>: 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.. :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. The by-product is that the code gets documented for free and the developers actually *want* to do it. :> :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. :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. :> :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. :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. 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. :> 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. :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. The other examples actually aren't applicable to the efficacy of DBC as they stem from errors in specification documents.. Don. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Don Harrison donh@syd.csa.com.au