Re: Safety-critical development in Ada and Eiffel

[Ken Garlington <kennieg@flash.net>]

Paul Johnson wrote:
> 
> In article <33CD6207.6007@flash.net>, kennieg@flash.net says...
> >
> >Paul Johnson wrote:
> 
> >> 1: Eiffel assertions are only executed at certain times, not at every
> >> invocation of a routine (see E:TL or OOSC2 for the gory details).
> >
> >OK, so Eiffel's different. What's the significant advantage of this
> >approach.
> 
> However if you call a routine from within a class, there is nothing to
> say that the assertions have to be maintained.  In fact it would be
> very restrictive to say that they must be.

OTOH, wouldn't I want the option to see if intra-class dependencies
cause
assertions to be violated? (Actually, in my case, I generally do want
this...)

Certainly, if I wanted to have my Ada exceptions raised only from an
external caller, it would not be particularly difficult to structure my
package to do this. So, other than maybe writing a little less code,
what's
the significant advantage of this approach? Is it safer to not enforce
assertions for intra-class dependencies?

I still don't see the big advantage from a safety-critical
perspective...

> >> 2: You can't inherit assertions.  Any such system would require lots
> >> of duplicated assertions.
> >
> >Why would I have to duplicate assertions?
> 
> Because of the Liskov Substitutability Principle.

To expand: Why do I have to duplicate assertions _in Ada_?

> >> 3: Invariants are still very tricky to support.  You need to call the
> >> invariant checks at the same time as the pre and post conditions.  See
> >> above for details of when this occurs.
> 
> >Again, I'm not trying to duplicate Eiffel. How much do I lose if Ada
> >invariants are different?
> 
> See above.

Ditto.

> >> 4: You had better be pretty sure that the compiler is not going to
> >> optimise your checks into oblivion during debugging, and conversely
> >> you need a way to turn them off for production code.
> >
> >Actually, I don't mind the checks being "optimized into oblivion" if the
> >compiler can deduce that they are unnecessary,
> 
> In many compilers, if you say "assert: require = (a > b)" then the compiler
> will observe that the value of "require" is not used thereafter, and
> remove the statement.

Since this isn't Ada, I couldn't comment.

> 
> >and I certainly don't
> >want
> >to exercise one kind of code during development and another during test.
> 
> The whole point of Eiffel assertions is that in a correct program they
> have no effect on execution.  Therefore you get exactly the same results
> whether they are enabled or not.

This would require (a) no changes in timing and (b) zero probability
that
the compiler generates incorrect code with a certain combination of
compiler switches and code. I am skeptical.

> Apart from assertion exceptions, the only way that the execution of an
> assertion can make a difference is if you call a function with side effects.
> Eiffel functions are specifically banned from having side effects.

See above.

> Of course, you *can* leave them enabled, but it slows down your code.

It does something else. It requires you to decide what to do if the
assertion is violated during execution.

> >If Eiffel compilers do no optimizations of assertions, and there are a
> >lot of complex assertions in Eiffel code, what does this say for the
> >efficiency of the code?
> 
> The point of assertions is to detect errors during debugging.  Some people
> leave preconditions on in production code as well, if there are no speed
> problems as a result.

What do they do if the assertion is violated?

> 
> >> [Difficulty of getting "short-flat" forms]
> 
> >Why would you want to _extract_ such information? The contract is in the
> >Ada specification in all of my code, at the level of detail I want
> >public.
> 
> No its not. 

You haven't read my Ada specs!

> The point of software contracting is that the public assertions
> are just that: public.  They are shown in the class interface (the short-flat
> form). 

Exactly. The Ada specification is just that: the public part. In fact,
it's
included in our software user's manual for OS-type software for that
reason.
It defines what the user needs to know, and nothing else. (Actually, we
do have to do one thing: we suppress printing of the private part, much
like
Eiffel uses documentation tools to extract the class specification.)

> Eiffel takes a different attitude to Ada here, and I can see the case
> for the Ada approach.  Instead of writing interface and implementation in
> separate files, Eiffel provides tools to extract the interface information
> from the implementation.  The public assertions are part of the interface,
> because they specify the class behaviour to its clients.
> 
> The Ada approach has the advantage that you can easily lock the interface
> while allowing changes to the implementation.  In Eiffel this could be
> achieved by recording the short-flat form of a class (the interface) and
> checking that the new short-flat form still matches after any change is made.
> Its just a bit more hassle to organise.

Right, although I don't the organization as a signficant issue. I would
be
more worried about making an inadvertant change, and failing to do the
check
afterwards.

Of course, I suspect you could acheive the same effect in Eiffel by
having the code
in multiple files, and using a CM system to merge the files as needed.

> 
> Part of the important thing about the short-flat form is that it includes
> *all* the interface information about a class, including any features inherited
> from ancestors.  This is important, particularly in the presence of multiple
> inheritance.  It means that programmers don't have to search through listings
> to reconstruct it manually.

> If you wanted to design a dialect of Ada with software contracting built
> in properly then you would have to bring the public assertions into the
> interface file.  And you would still need the equivalent of "flat" to bring
> all the ancestor features into your class.

You can do this in Ada, too, with the proper documentation tools. It's
just
a bit more of a hassle to organize :)

> 
> Paul.
> 
> --
> Paul Johnson            | GEC-Marconi Ltd is not responsible for my opinions. |
> +44 1245 242244         +-----------+-----------------------------------------+
> Work: <paul.johnson@gecm.com>       | You are lost in a twisty maze of little
> Home: <Paul@treetop.demon.co.uk>    | standards, all different.