Re: Safety-critical development in Ada and Eiffel

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

Ken Garlington wrote:

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

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?


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

That *is* hideously crude (and brings back some bad memories). Depending on how
crude you mean, maybe a primitive tool could give you a map of where objects get 
put in memory. If you mean incredibly crude, use non-reference (expanded in 
Eiffel) types and use a linker-generated memory map.


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

You would use them anywhere that a piece of code makes assumptions. For example,
to help avoid the Ariane fiasco, include contracts in the INS(?) that specify 
Ariane 4 dynamics. Then, in testing, you will get an assertion violation when
you apply Ariane 5 dynamics to it.

:Again, the code I've seen to date doesn't seem to use them that much.

If you're looking in Ada code, you're looking in the wrong place because few
Ada developers recognise there are additional benefits from using them in 
addition to static typing and the predefined contracts already in Ada 
(the conditions under which predefined exceptions - eg. Constraint_Error - 
are raised).

Static typing gives you static contract checking. Assertions (predefined and
user-defined give you dynamic contract checking *during development*. What 
most Ada software engineers miss out on is the user-defined variety which 
bring a non-trivial benefit to reliability and reuse.


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

They are only turned on during development, so what you do is fix the underlying
problem which is usually not difficult to find if you've used them systematically.
Even if you haven't (I was the only one of a team of 5 using them in our recent
development cycle), they still tell you more than you would otherwise be told.

Good design complemented by static typing and Design by Contract is unbeatable, 
IME.


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

Right. However, only an incorrect program will raise assertion violations at
runtime. As you systematically identify and fix the errors causing them during
development, you can turn assertions off with confidence when the system 
goes live. Then, any errors you may have missed will be handled by exception
handlers in the usual way.
 
:Static assertion checks, of course, can be
:detected and
:corrected during development, which is why I like Ada's strong static
:type checking.

I agree completely. Static typing is great but it isn't the *whole* story.


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

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


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


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

IME, they do.

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

I disagree. It takes me about the same amount of time to specify an Ada
subtype as it does to specify a more general assertion. Even if the general 
assertion is a function, I would more than likely need to write it anyway so
would have expended the effort anyway.


:However,
:in both languages, overuse of assertions may be just as bad as underuse.

It is possible to overuse them but 99% of developers err on the othger side. :)


:(As you can tell, I'm somewhat of an assertions heretic. 

That's fine but have a go at using them where appropriate. I'm sure you'll 
become convinced.

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

No use of assertions will stop you misinterpreting requirements. They're not 
a magic wand but they *will* help you remove a class of errors you would 
otherwise miss.


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

Come on. He's not saying that.


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