Re: Safety-critical development in Ada and Eiffel

[Ken Garlington <kennieg@flash.net>]

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