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: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,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/22 Message-ID: X-Deja-AN: 258078859 Sender: news@syd.csa.com.au X-Nntp-Posting-Host: dev50 References: <33CFFAF7.6834@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-22T00:00:00+00:00 List-Id: Ken Garlington wrote: :Again, someone needs to explain how these high-level assertions would :have :benefitted the Ariane 5 IRS. I have almost zero interest in the Ariane failure because (as Robert Dewar correctly pointed out some time ago) it reveals next to nothing about software engineering except what is blindingly obvious. :> So, here's a different example. In my key handling object (one of the highest :> level in the simulation), there's an operation for interpreting the CLEAR key. :> Simplifying a little, pressing this key should reactivate the menu, clear the :> key sequence and clear any menu or sub-menu selection. So, there's a compound :> postcondition thus: :> :> if SA.ASSERTIONS_ON and then (INPUT_STATE /= MENU or else :> NO_OF_KEYS /= 0 or else MENU_OPTION_SELECTED or else :> SUBMENU_OPTION_SELECTED) then :> raise SA.POSTCONDITION_ERROR; :> :> Note that some of the components are functions. Wrapping them in this way :> is typical practice in Eiffel and enables you to use them elsewhere (eg. in :> if-statements in the code proper) and makes contracting scalable. : :In Eiffel, I assume this code would be in the "short form." Is the :user/reviewer :really expected to read all of this (including looking up the functions :embedded :in this code) and understand it? 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. Second, the compound condition represents a single higher level condition which can be declared as a function. So, expressing it in Eiffel and wrapping the compound condition, we have ensure in_menu_state with function in_menu_state defined as in_menu_state: BOOLEAN is do Result := ... -- compound condition end. This should be simple enough for any reviewer. The meaning of in_menu_state is self explanatory but if they want more detail, they can look at its implementation. :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? :... So, unless you propose teaching DBC :to all engineers in the program (which might not be a bad idea, :actually), I agree, it would. :> With regard to whether an Eiffel software engineer would have :> picked up the false assumption compared with an Ada SE - possibly, due to the :> fact that they are conditioned by their use of contracting to *think* of as :> many assumptions as possible so they can code them as assertions. This sort of :> conditioning is much less prevalent among Ada developers because most don't :> use contracting (in this disciplined sense). I *know* this is true because I :> work with them. Of course, they may be (and probably are) more disciplined :> in your domain simply because they *have* to be. However, the conditioned :> cultural difference due to disciplined contracting would be an advantage. : :Our engineers are taught the same thing in ADARTS, so I don;t think this :is :as big a difference as you think. 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. :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. :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!.. :> For your domain it's a bit of a Catch-22. Contracting would improve the culture :> but you're unable to use it due to hard timing constraints. : :Not at all. We have to distinguish between "contracting" and :"assertions." You :can still think in terms of writing strong interfaces, with well :documented :user constraints (ADARTS term), but without coding them. For example, :you may :write your test cases such that pre-conditions, post-conditions, and :invariants :are checked outside the object code. You can also permit more :comprehensive :reviews by documenting them via comments. The point is, you don't have :to use :DBC/Eiffel to get these benefits... they are also contained in :ADARTS/Ada, for :example. 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. :> No, it's the conditioning that makes the difference. There are a lot of :> Ada software engineers who *are* serious about quality (including you, I expect). :> Using DBC just makes you more effective. : :However, the supposed advantage of Eiffel is that this thinking becomes :code. :I don't see the advantage for my domain (although I certainly do for :others). Agree. [...] :> Can you give an example? Not sure how high-level you mean. : :Recent examples: : : Ariane 5 - incorrect operational profile (Ariane 4 specified instead :of 5) : See: :http://www.esrin.esa.it/htdocs/tidc/Press/Press96/ariane5rep.html 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 BTW, this is intended to suggest what ought to done in engineering such software. This presupposes (among other things) that someone has actually sat down recognised the dependency of the IRS on the rocket dynamics. It is *not* a slap-on "remedy" to the non-existent software engineering that was practised in reality. : F-18 - divide by zero at Mach 1, due to incorrect control law :equation in spec. There already was a predefined assertion for this - "you may not divide zero" - which presumably resulted in a numeric_error. This assertion correctly exposed an incorrect formula(?). : YF-22, Gripen - PIO due to incorrect control law equation in spec. : (PIO is a complex lag interaction between the operator and the system - class SOME_CLASS ... invariant not PIO (..) end Likewise, this would expose the incorrect formula. :Aren't there more fundamental problems than just this? You state that :the assertions can't be executed in a hard real-time thread, so how does :a "realtime" library help? For those that aren't. Don. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Don Harrison donh@syd.csa.com.au