Re: Safety-critical development in Ada and Eiffel

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

Sorry, this response is interminably long...


Warwick Pulley wrote:

:Don Harrison wrote:

:> BTW, how do call a procedure under different names in Ada?
:
:By declaring a procedure that "renames" the old one, eg...

Yes, I should have realised! It's the old workaround to the infuriating Ada83 
visibility problem of not being able to see the predefined operators of a user-defined(?) type in client code. In spite of already with-ing the 
supplier module (which I don't think you should have to do, anyway - if you 
*use* features exported by a package, explicitly importing it is redundant), 
you can't see (hence, use) the imported operators.

While Ada95 has ameliorated this restriction via the "with <type>"(?) statement,
it doesn't go far enough, IMO. Better would be removing the need for any
explicit importation of operators. Even better, IMO, would be removing explicit 
imports of everything (including packages). However, I guess the existence 
of "use" clauses would then create ambiguity problems. Never did like "use" 
clauses.

Interestingly, this issue reveals a benefit of unifying module and type. 
A unified model that dictates unique class names (eg. Eiffel's) simplifies 
things by allowing class names to serve a twofold purpose in clients - 
importing modules and entity (variable or routine parameter) declarations.
In one fell swoop, the need for import statements ("with"), visibility 
statements ("use"), and module prefixes for diambiguation disappear.

WRT renaming operations, I'm not sure whether the current semantics provide 
the same capability as Eiffel. For that to be the case, it would need to allow
synonyms in *declarations* as in the Eiffel declaration of the equality 
operator (overlooking the anchored type):

  equal, frozen standard_equal (some: ANY; other like some): BOOLEAN is..

[This declaration gives you a common declaration for a redefinable - "equal" -
and a non-redefinable operation - "standard_equal". In a mission-critical system,
where you wanted to force static binding, you could use the frozen version in 
calls and use the redefinable version to specialise when inheriting.]

A cursory glance at the Rationale - 8.3 suggests you may be able to do this 
but I'm not sure.

BTW, I recall reading somewhere in the Rationale that Ada allows some sort of
anchored type declaration. Anyone care to give an example?..


:> 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).

Yes, that's particularly an issue in mission-critical HRT domains such as Ken's
(spacecraft(?)..). For domains where timing is less critical such as ours 
(simulators), it becomes a viable tool. I should reiterate (in case it's been 
forgotten) my original suggestion that individual threads *within* an HRT system 
may be medium RT and hence candidates for Eiffel-style contracting. This implies
an architecture in which threads may be allocated to specific processors of 
multi-processor hardware. In this way, the HRT threads can happily do their 
stuff without risk of interference from slower threads. This reality of this
scenario depends, of course, on the timing requirements of inter-thread 
communication.


:I imagine that one needs to take special care when using assertions in
:languages that don't fully support them.  

Definitely, and I would hope GNAT, for example, allows you to use assertions
without enclosing if-statements or compiler directives like 

  begin
    assert (<boolean_expression>)           -- precondition
    ...                                     -- actual body of routine
    assert (<other_boolean_expression>)     -- postcondition
  end;

and allows you to turn them on or off via a compiler switch. Is this true?


: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.

Yes, the above would look like

  require <boolean_expression>              -- precondition
  do
    ...                                     -- actual body of routine
  ensure <other_boolean_expression>         -- postcondition
  end;


:While this argument favours Eiffel in terms of assertions, it doesn't
:mean that porting this functionality to Ada will not introduce other faults.

Sure. It's best to use a technique that minimises the risks - hence my 
expectation of what GNAT provides.


: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 agree and this certainly isn't my prefered way of emulating assertions. 
I would much prefer to use the technique I described above but doing so 
with our Ada83 Verdix compiler would require using compiler directives to 
wrap each assertions. As this, would be messy, I chose to use if-statements
where the conditional expression was a short-circuit boolean expression.
This represented a minimal risk to correctness (the first component is 
Assertions_On so the rest is ignored if set to False) and a small execution 
overhead acceptable for our medium RT domain.


: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.

I expect you are referring to my own error (actually it was two) in which 
I coded the incorrect logic. I hope you'll allow me a few mistakes. After all,
these were the only two extant miskakes following integration out of 172 
such statements. That implies 98.84% were logically correct which, you'll 
agree, isn't too bad. What this does reinforce is that assertions do not 
obviate the need for testing but are a tool to help facilitate it.

BTW, assuming what you say is correct, the assertions were turned off and 
the code handed over to the testers without my knowledge. I would have tested
it first.

: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.  

..*especially* for such languages.

: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.

Certainly.

: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.

Neat idea. What a pity you didn't think of it back in February! Maybe we could 
use it next time if we don't have something better..


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

Yes, although the amount of self-discipline to use it effectively is small.
To eliminate that entirely, best use the real thing. :)


: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.

Sure. I suppose if anyone is going to emulate assertions in ways that may 
affected by compiler optimisations, it would be wise to become acquainted 
with these so you know what you're in for.


: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.

Yes, I suspect this is usual practice.


:> :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?

Your right - this is mis-phrased. It should be:

  "However, I found I was spending about a third of the time integrating 
   compared with my colleagues which meant I was saving time overall. Despite
   spending less time integrating, my code was more reliable."


[...]

:BTW, how do you verify the correctness of your assertions, 

You already have a built-in assertion checking mechanism in the code proper
because if an assertion is incorrectly coded, it will raise an exception 
in *valid* circumstances rather than invalid ones. If you know that the 
context is correct, examination of the boolean expression cin the assertion 
will very quickly show you what the problem is. The upshot is that you have 
to think catefully about what the valid underlying assumptions are in the first
place and debug assertions that reveal incorrect assumptions or simply coding
errors.

:and that there are
:no errors that the assertions didn't find?  

You can't verify that of course. You can't express everything as an assertion
and their use doesn't obviate the need for testing. Rather, they help 
facilitate testing.

: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?  

Both of these. To ensure code coverage, I used the debugger to check that 
the right brancehes were executed in the right circumstances.

:Either way, a documentation
:of your method would provide a good test which can then be reproduced should
:the software be modified.

Yes, that would be a good idea. Not just now though - I have some test reports
to write!  :)


Don.
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
Don Harrison             donh@syd.csa.com.au