Re: Safety-critical development in Ada and Eiffel

[donh@syd.csa.com.au (Don Harrison)]

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