Re: Safety-critical development in Ada and Eiffel

[warwickp@syd.csa.com.au (Warwick Pulley)]

In article <33CD1722.2D24@calfp.co.uk>, Nick Leaton <nickle@calfp.co.uk> writes:
> Warwick Pulley wrote:
> 
> > I have seen this happen at least once, where an executable was released to
> > the test group which AFAIK was only tested with assertions enabled, and then
> > it was discovered that a crucial line of code was removed because it was
> > within an assertion block and once this error was encountered the executable
> > didn't crash but its functionality was imparired severely enough so that
> > it had to be run again.
> 
> Can you explain this a bit more. In Eiffel an assertion has to be 
> a boolean expression, and I presume that you are not writing a 
> boolean expression that has a side effect?

Personally I haven't used assertions to their full extent although I like
to have error checking in place.  It turned out that the problem lay not in
the boolean expression itself, but how it was used.  The example I was
referring to above, which was also modelled in Ada, was not of the
form:

    -- example 1
    if <assertions on> and then not <check> then
      raise <postcondition error>
    end if;

    return <value>

but looked like:

    -- example 2
    if <assertions on> and then <check> then
      return <value>
    end if;
    raise <postcondition error>;

This of course worked fine when assertions were on because when the check was
satisfied a value was returned and the assertion was avoided.  When assertions
were switched off and the procedure got called, an exception was raised
unconditionally and broke the software during testing.

I my last post I mentioned a method of using assertions in Ada to address this
problem, namely by using *one-line* calls to inline precondition and
postcondition checking procedures.  They also had the advantage that the
assertions could be included only when a compiler directive was set to TRUE,
rather than using a boolean statement.  When assertions were off, the body of
the procedure would be a "null;" statement which would get optimised out.  I
hope.  :)

Example 2 above is an example how the assertions can be "mis-implemented" in
Ada, because the logic is wrong and necessary code was included in the "if"
statement.  As you have said, all you need in Eiffel is the boolean
expression itself, and since Eiffel has a special clauses for these
assertions it's not possible to include vital procedural code within these
clauses.

Although I made the point about Ada specifically, I then made it
unnecessary by making the broader statement that I would be uneasy about
releasing software that was untested with assertions removed.  This would
be whether the language I program in supports assertions or not, and I
guess the same goes for any software that's released in a different form
to which it is tested.

> -- 
> 
> Nick

Regards,

Warwick.