Re: Safety-critical development in Ada and Eiffel

[Ken Garlington <keg0@flash.net>]

Don Harrison wrote:
> 
> If even this small overhead is unacceptable, you can force static binding
> where necessary by freezing routines.
> Although you forgo the flexibility of
> polymorphism, you can still take advantage of inheritance by virtue of Eiffel
> synonyms - these allow you to declare a routine under different names.

But I can do this in Ada, as well, so I don't see the benefit.

 :Does this "pre-allocated memory pool" mean that you will know exactly
> :what address
> :each object's data will reside at, or merely that you dynamically
> :allocate memory
> :at initialization and do not dynamically allocate after initialization
> :is complete?
> 
> The latter. You don't actually need to know *where* objects are allocated,
> merely that there is sufficient memory to allocate them.

Actually, in my systems, I do need to know where they are allocated, so
that
I can examine them from the hideously crude display in the cockpit
during
troubleshooting.

> Maybe general assertions are more common than you imagine. However, I agree
> that range constraints are roughly covered by Ada subtypes. I use them liberally
> for just that purpose.

Maybe, but again, I would like to see how these complex assertions are
used. Again,
the code I've seen to date doesn't seem to use them that much.

> Correct me I misunderstand you.. Are you wondering whether contracting
> helps you to identify more bugs? I can offer my own experience which has
> firmly convinced me of this.

Contracting definitely identifies more bugs. However, my concern with
Eiffel
assertions (and Ada assertions, for that matter) is that, once raised,
it's
not always clear what to do about them. In a safety-critical system such
as
we build, you can't just generate a core dump, or ask the user what to
do next.
You have to generate a correct response to the assertion failure, and
you have
to do it very quickly. Static assertion checks, of course, can be
detected and
corrected during development, which is why I like Ada's strong static
type checking.

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,
or more
likely code generation errors) to have much confidence in this approach.

Another consequence of using assertions is that you have to develop and
test the
assertions. As a result, you need confidence that the benefits of the
assertions
outweigh the dilution of your test effort. One of the advantages of
Ada's simpler
approach (at least, it seems simpler to me) to simple
pre/post-conditions (range
checks in particular) is that the cost of adding them is somewhat
reduced. However,
in both languages, overuse of assertions may be just as bad as underuse.

(As you can tell, I'm somewhat of an assertions heretic. However, I will
say that
for non-real-time, non-safety-critical systems, they are outstanding. My
tool code
is lousy with them.)

> Consequently, when we (a team of 5) recently
> reached the end of a 5 month long development effort of incremental coding
> and integration testing, the parts of the system that used contracting work
> flawlessly apart from problems resulting from misinterpretation of requirements.

Most of the problems we see in formal testing are from misinterpretation
of
requirements - which is another issue I have with assertions as a magic
safety wand.
Of course, Bertand Meyer's Eiffel website insists that even
misinterpretation of
requirements (Ariane V) will be a problem no longer when Eiffel is used!
:)