Re: Safety-critical development in Ada and Eiffel

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

Don Harrison wrote:
> Ken Garlington wrote:
> 
> :But I can do this in Ada, as well, so I don't see the benefit.
> 
> I'm not saying there is any extra benefit - merely that you don't have to 
> wear the overhead of dynamic binding if you're desperate to maximise efficiency.
> Tucker mentioned that overhead. I'm saying it isn't an issue.
> 
> BTW, how do call a procedure under different names in Ada?

By declaring a procedure that "renames" the old one, eg.

procedure ADD_ONE(X: in out INTEGER);
procedure INCREMENT(X: in out INTEGER) renames ADD_ONE;

<large section snipped>

> :There is a school of thought that says to add in assertions, test the
> :system, and
> :then remove/suppress the exceptions. I have seen too many cases of code
> :that works
> :with the assertions active, and then breaks (due to timing differences,
> 
> Yes, timing *is* something to be concerned about when applied to realtime 
> systems. That's why I suggested not using assertions in the hard realtime
> threads of a process. BTW, software designed using DBC may actually run *faster*
> than code without it because you get to strip out all the defensive validity
> checks. You have already ascertained during development that operations are
> called in valid contexts so you don't have to check the context.

In Eiffel that may be true provided that removal of assertion checks doesn't
significantly affect the performance of the code in any way.  The issue of timing,
mentioned by Ken above, is a good example).

I imagine that one needs to take special care when using assertions in
languages that don't fully support them.  From my (sorely lacking!!) knowledge
of Eiffel, clauses that define the precondition and postcondition of an
operation contain exactly one boolean statement which automatically restricts
the coder from including procedural code within these sections.

While this argument favours Eiffel in terms of assertions, it doesn't
mean that porting this functionality to Ada will not introduce other faults.
With Don's demonstration of assertions last Friday (Jul 11 18:05:13 EST) the
postcondition was implemented in the form:

if <assertions on> and then <bool_postcondition>
  raise <postcondition exception>
end if;

The implementation of the assertion is done with multiple statements, so
there is the possibility of important sections of code being inadvertently
added within the "if" statement which would then be removed when assertions
are disabled.

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.

Even one error, however minor, is enough to warrant another round of
testing after assertions are removed: at least for languages that don't
fully support assertions.  Even if no errors are discovered in the process
I would consider it a worthwhile exercise, if only to convince myself that
the software functions how I intended.

A suggestion: to avoid some of these problems one could have written two
procedures, say 'precondition' and 'postcondition', each having an 'in'
boolean parameter.  Each procedure should do nothing if assertions are
disabled, but if they are enabled then they would raise the appropriate
exception if the 'in' parameter was false.

Then rather than the above block, one could evaluate a postcondition
by the call:

postcondition(<bool_postcondition>);

and similiarly for preconditions.  A sample implementation of 'postcondition'
(in pseudo-Ada) is:

--------------------------------------------------------------------------------

procedure postcondition(requirement: in boolean) is
begin

# if <assertions on> then

  -- check condition and raise exception if violated
  if not requirement then
    raise <postcondition exception;>
  end if;

# else

  null;

# end if;

end postcondition;
pragma INLINE(postcondition);
--------------------------------------------------------------------------------

So when exceptions are disabled (via a compiler directive), 'postcondition'
would have a null body, and since it's inline there would be no unwanted
procedure call.  It also means that you can conditionally compile
assertions without having to surround each assertion with conditional
compilation directives.

Naturally, my suggestion above still fails to prevent the addition of code
before a precondition check, or after a postcondition check, etc.

> :or more
> :likely code generation errors) to have much confidence in this approach.
> 
> If that's a problem, you need to get your vendor to clean their act up.

Yes, if you know the compiler has a bug in the first place.  The trouble is
that you don't know it's a problem until it occurs, and a compiler could
have a subtle bug that only occurs in very particular circumstances.

Although any respectable compiler has minimal bugs if any, if we don't test
our products after assertions are suppressed then we unnecessarily transform
our confidence in, into dependence on, the vendor's compiler to function
correctly.

It would be irresponsible to deliver software that has only been tested with
assertions enabled, knowing that if an error occurs in the released version
then it's "not my fault".  So for this reason, and for peace of mind, I would
certainly test the version of the software to be delivered to the customer.
Since we expect not to find more errors, this last phase would run smoothly
and quickly.

> :Another consequence of using assertions is that you have to develop and
> :test the
> :assertions. 
> 
> Correct. My initial reaction when I started using them was "Gee, I've got to
> do this extra work on top of writing the "real" code! However, I found I was 
> spending about a third of the time integrating compared with my colleagues
> which meant I was saving time overall and producing more reliable code to boot.

Why should a short integration period automatically imply code reliability?

> :As a result, you need confidence that the benefits of the assertions
> :outweigh the dilution of your test effort.
> 
> IME, they do.

I agree that some type of error checking is in order during development.  I
suppose that whether the results of a failed check is done in the form of a
text message, raising an exception or by other means is a matter for another
thread.

BTW, how do you verify the correctness of your assertions, and that there are
no errors that the assertions didn't find?  Do you prefer code inspection,
or if you do your verification by executing the program itself, how do you
ensure that each section of code is exercised?  Either way, a documentation
of your method would provide a good test which can then be reproduced should
the software be modified.

Happy coding,

Warwick.