Re: Safety-critical development in Ada and Eiffel

[Ted Velkoff <velkoff@erols.com>]

Ken Garlington responded to an earlier post of mine:
> 
> This is certainly reasonable. However, once the execution capabilities
> are removed, it seems fair to ask what Eiffel provides that comments
> (available in most langauges) don't provide. If there is not a
> significant
> difference, then Eiffel would not be any better (in this context) than
> any other language, so long as the DBC principles were followed.
> 

In my experience, there is a significant difference.  I will not presume 
to make a scientific claim; rather I will offer a personal, anecdotal 
example.

About two years ago, I built a modest enhancement to a system which 
amounted to 4K lines each of Ada and C++.  In the package specs and 
module headers I included preconditions, postconditions and invariants 
as comments.  In the Ada bodies, I wrote if-then-else clauses to test 
preconditions (violations led to a chain of exceptions raised out to 
the main program).  In the C++ implementations, I included conditionally 
compiled calls to the assert macro (which does a core dump and spits out 
a file and line number) for preconditions and trivial 
postconditions.

This approach worked really well for me because I was very motivated and 
willing to do certain things.  Those things included: Step 1) write the 
assertions as comments in the specs; Step 2) update comments in the 
specs when testing revealed missing assertions (it's against the rules 
to introduce a precondition and not tell anyone about it - a contract 
with secret codicils, so to speak); Step 3) write the code to test the 
conditions, raise exceptions and generate a trace (in the Ada code).  

This approach was not without flaws:  Flaw 1) In the Ada code, for 
instance, there was no conditional compilation; to remove the assertion 
monitoring would have been a tedious exercise;  Flaw 2) I didn't even 
attempt to monitor postconditions - this is harder, even for simple ones 
(e.g. count = old count + 1); Flaw 3) as implied above, information had 
to be kept in synch in two places: the specs and bodies.

In my opinion, this won't scale up to a large team.  20% might see the 
benefit and be willing to do the many tedious manual tasks I described; 
20% will see no benefit, and even if they did, wouldn't do it; the other 
60% could be persuaded that it would help but wouldn't tolerate the 
extra upfront burden and wouldn't adopt it (in particular, steps 2 and 
3).  I should say I haven't tried it out on a team; this is pure 
conjecture.  (If anything, this appraisal is optimistic.)

Meanwhile at home I write software in Eiffel, where assertions are built 
into the language.  In Eiffel, all I do is Step 1: write the 
pre/post-conditions and invariants.  I don't need to do Step 2 (keep 
spec and body in synch) since in Eiffel, the spec (properly speaking, 
the short form) is automatically generated by tools.  Step 3, (coding 
the assertion tests, handling failures, providing useful diagnostics) is 
provided automatically by the environment.  Furthermore, the three flaws 
are eliminated: 1) with a compile-time switch I can turn off monitoring 
(I don't have to go through and "comment out" reams of code); 2) it's 
easy to monitor post-conditions, since this is provided by the tools 
(caveat - this is useful for testing and integration; postcondition 
monitoring necessarily incurs a performance penalty); 3) mentioned 
above, there is no spec/body redundancy to be managed by the programmer.

Returning to my view of scalability, I think the same 20% of 
programmers would love to work in a programming environment with these 
capabilities, 20% would still dislike it; but the other 60% - I think 
they would like it.  I say that because the cost/benefit is easier to 
see.  It doesn't take much time to write assertions, so when the rest 
comes for free (documentation and testing), programmers will want to 
write them.

Finally, I'll contrast Eiffel's assertions with comments (in any 
language).  I conjecture that because they can be monitored easily, 
Eiffel's assertions affect programmer psychology.  As a supplier, if I 
write postconditions or invariants as comments, I might be merely making 
promises.  If I know those assertions are easily monitored, I will be 
careful about what I promise: the auditor might show up at any minute.

I can imagine that Eiffel may not be suitable for certain real-time 
applications mentioned in this thread.  Nevertheless, I am convinced 
that a large number of software projects would benefit from employing 
"Design By Contract", and that Eiffel is the only language I know 
that makes its application practical and cost-effective 

-- Ted Velkoff