Re: Safety-critical development in Ada and Eiffel

[Ken Garlington <kennieg@flash.net>]

Paul Johnson wrote:
> 
 How?  It sounds like you would have to have internal and external
> versions of all routines, all suitably redefined in the presence of
> inheritance.  This is not a trivial suggestion.

Seems fairly trivial to me, particularly since I only have to worry
about this in certain cases.

> >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?
> 
> Suppose I have an invariant in my class: "foo (a, b) = 0"
> 
> This states a relationship between a and b.
> 
> Now my class could have one routine which computes both a and b
> simultaniously.  Or it could have one routine which computes a, and
> another routine which computes b.  This is purely an internal
> implementation decision, so I should be able to chose either.
> 
> But if I have in my class the following two lines
> 
>    compute_a;
>    compute_b;
> 
> then under your scheme I will get an exception.  As "compute_a" terminates,
> the invariant will be checked, and will fail.  So the public assertion
> constrains the private implementation.
> 
> (Actually, its even worse.  If I assign to a and then call any
> routine before assigning to b then I'll trip the invariant check)

Since I can structure me system to only perform the invariant from
an external call, this doesn't seem to be a big issue...

> 
> >I still don't see the big advantage from a safety-critical
> >perspective...
> 
> The Eiffel rules for assertion checking allow the software to be laid out
> in the most logical manner, making proper use of functions and procedures.
> This helps the programmers avoid bugs.

But that's an argument from assertion checking in general (which
Ada also supports). What's the big deal about having to write a
little extra code to only have certain assertions exercised from
external calls? The only difference is that Ada does internal
checks by defaults, Eiffel requires extra code if you want the internal
checks.

> 
> >> >Why would I have to duplicate assertions?
> >>
> >> Because of the Liskov Substitutability Principle.
> >
> >To expand: Why do I have to duplicate assertions _in Ada_?
> 
> Well, Ada these days has inheritance.  If you want to write correct
> software then descendants must inherit their ancestors contracts.
> If you want to check and document this then you have to write the
> appropriate assertions.

You have to write the appropriate assertions in the ancestor, in
either Ada or Eiffel.

To repeat: Why do I have to _duplicate_ assertions in Ada?

> >> 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.
> 
> This discussion started when someone (I assumed it was you, sorry I didn't
> check) proposed a type "require" defined as a subrange of Boolean constrained
> to be true.  The above statement declares a variable "assert" of type
> "require" and initialises it to "(a > b)".  If this expression evaluates to
> false then a range exception will be triggered.

ah... assert : require := (a > b);

However, this shouldn't be optimized out if an exception is possible, I
don't think. (I'd have to go look back at chapter 11 to be sure...)

>  Sorry if I've got the
> syntax wrong, and sorry that my explanation was wrong as well: I should have
> said "... the value of 'assert' is not used thereafter ...".
> 
> Of course there are other ways of writing assertion checks in Ada.
> 
> >> 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
> 
> If your software depends upon timing for the correctness of its results
> then I would certainly not want to see your software used in safety
> critical applications.
> 
> I agree that timing variations can cause different results, but why would
> they cause incorrect results?

Because you made a mistake, of course! A mistake which will be hidden
during
your testing, but become (potentially fatally) obvious during
operational use.
This is considered a Bad Thing.

>  If they don't cause incorrect results then
> why are you worried?

Because I won't know whether or not the actual system is correct or not!

> >and (b) zero probability
> >that the compiler generates incorrect code with a certain combination of
> >compiler switches and code. I am skeptical.
> 
> What does this have to do with the problem under discussion?  I agree that
> this can happen, but why does the ability to enable and disable assertions
> cause any new problems?

Because I have seen compilers that generate correct code with one set of
compiler options enabled, and a different (incorrect) set with a
different
set of options enabled. As with the timing issue above, I can do all of
my testing with assertions enabled, and have no clue whether or not the
code will still work after I disable those assertions (due to a compiler
bug). Again, this is a Bad Thing for safety-critical systems.

> 
> >> 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.
> 
> Functions that might have side effects are fairly easy to detect (they
> assign to non-local variables, or call other routines that do so).  This
> can be statically checked.
> 
> Sometimes a function will cache a result for future use.  I've written
> table classes that do this.  Such functions are fairly rare.  When detected
> by static checks they can either be inspected carefully or simply banned.
> 
> >> 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.
> 
> Surely the same arguments apply to Ada?  Look at Arianne 5.

Yes, they certainly do (and I have applied them to Ada in comp.lang.ada
in the psat). Of course, this discussion isn't about Ada vs. Eiffel, is
it?
It's about the usefulness vs. the risks of using assertions in safety-
critical real-time systems. Eiffel claims it's big advantage over other
languages (including Ada) in this domain is stronger assertions. This is
not a particularly useful claim if there are serious problems with using
assertions extensively in such systems, is it?

> 
> >> 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?
> 
> Depends on the application.  Generally they print an error report, dump
> stack information to a file, and ask the user to phone the vendor.  Note
> that I am not proposing this for real-time embedded applications.  However
> there are safety-critical applications which are not real-time.

True. Furthermore, there are safety-critical real-time applications that
are not required to be fail-operational. In both cases, I can at least
see
the glimmer of hope that assertions might have some value. (However,
even
a non-real-time system monitoring a nuclear power plant, for example,
might
not want to print out a message saying "phone the vendor, and I hope the
reactor doesn't go supercritical while you're on hold :)

However, for _at least_ certain classes of safety-critical systems, this
behavior is completely unacceptable. Unfortunately, most people who
advocate
liberal use of exceptions are working on systems where it is quite
acceptable.

> 
> >> >> [Difficulty of getting "short-flat" forms]
> 
> >You haven't read my Ada specs!
> 
> Are you saying that you write the contract in comments in the spec?  If
> so then good for you: its good practice.  The problem is that you have
> now duplicated the information: one copy is in comments, and the other
> is in the assertions in the code. 

Actually, no: the public (abstracted) view of the assertion is in the
spec,
the implementation is in the code. This allows me to change the
implementation
any way I want without affecting the client, so long as I meet the
_requirement_
for the assertion.

> Hence you have doubled the associated
> work, and increased the risk of an error.  Eiffel requires that you write
> the contract once, and uses the text for both purposes.

Which is less writing, but may also require the user to see details that
are not necessary. (There's no obvious "best" answer here in my mind,
but
both approaches seem to be satisfactory from a safety standpoint.)

The other advantage in comments is that they won't affect the object
code. Thus, I can put in a user constraint, but not enforce it in the
code,
if I want. (I can enforce it in other ways; e.g. in a debugging
environment). This allows me to compromise between no assertion
capability
at all, and having assertions that affect my object code in unwanted
ways.
Particularly for complex constraints, comments may actually be more
safe in this environment. (Simple constraints, of course, can be coded
in
type information and checked statically, even if no dynamic checking is
done.)

> 
> I'll agree that all of the benefits of Eiffel assertions are available
> in Ada if you put in enough work, but why all this effort to do something
> that Eiffel does automatically?

As noted before, there doesn't seem to be much difference in the Ada
work
vs. the Eiffel work, particularly since there are limitations to the
amount of assertions to be embedded in the code for safety-critical
systems.

>  Also if the work becomes too onerous
> then it tends to get dropped when schedule and budget pressure is on.
> This has been the vice of software engineering ever since the discipline
> was invented.  Eiffel makes good practice so cheap, easy and obvious
> that people do it without needing to make a special point of it.

However, this extra capability does me no good if I can't take advantage
of it.

> 
> [Stuff about deriving documentation from specs deleted: we seem to be in
> broad agreement]
> 
> 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.