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: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,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/21 Message-ID: <33D43D93.6A8E@flash.net> X-Deja-AN: 258083054 References: <33CFFAF7.6834@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-21T00:00:00+00:00 List-Id: 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? > 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? For that matter, if this is the correct method, why not do it in Ada? > ..and lose the benefit of being able to execute it? According to Meyer, the principle benefit is the documentation value. 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/ > :... 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. > 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? > > :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? And what does that do to the oft-said statement that Eiffel programmers put in assertions for unlikely events? > :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. How do you catch software design faults in your code if you assume you made no mistakes in your 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. > 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. 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. > 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(?). But how would the user write an Eiffel assertion to cover this? I know that Ada has pre-defined assertions, but how does the Eiffel coder write an assertion that says "this equation has no errors?" > > : 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. Unfortunately, PIO is not a formula, nor can it be sensed by the system. It is an interaction between the operator and the system. The system sees the operator telling it to ascend, then descend, then ascend a little faster, then descend faster still... which might be valid commands. However, what is actually happening is that the pilot's sensory system is a little behind the dynamics of the airframe. He's trying to level the aircraft, but he's actually making the problem much worse. There are criteria that can be used to analyze a system for such potential behavior, but overcompensating for PIO can make the system too stable (not responsive enough). Try writing a post-condition that says, "user's favorite color displayed on screen" (without being able to ask the user first) and you'll see what I mean. > > Don. > =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- > Don Harrison donh@syd.csa.com.au