Re: C.A.R. Hoare on liability

[dewar@gnat.com (Robert Dewar)]

"Robert I. Eachus" <rieachus@attbi.com> wrote in message news:<3D1390D0.7040709@attbi.com>...

> I agree with the point, but not the example.  For Ariane 4, the analysis 
> was carried out, and whether or not you agree with the final decision 
> for Ariane 4, the decision was well thought out.  The disaster was that 
> the Araine 4 analysis was carried out absent the Ariane 5 requirements 
> for political reasons, and the Ariane 5 requirements analysis was never 
> done.

I disagree. Here you have a case in the Ariane4 code where a check was being
made at runtime which had the quality that if the check failed, disaster
would occur. There are two possibilities

1. In the Ariane4 code, it was demonstrated that this check could never fail.
In that case, the check should not have been there.

2. In the Ariane4 code, it was NOT demonstrated that this check could
never fail. In that case, they were just lucky that no Ariane4 blew up.

I will repeat. You should NEVER have a runtime check in your code where it
is the case that failing the check is a more serious situation than not doing
it at all. Casually putting in checks is very likely to generate such cases.

My understanding of the Ariane case is that this check was casually put in,
in other words it was put in WITHOUT any analysis that said this check was
needed. Deployed code should not have such checks.

If you leave checks on throughout an Ada program, then a complex analysis is
required to ensure that if any check fails, it is properly handled in a manner
that does not do more damage than failing the check.

If you do not leave checks on, then a complex analysis is required to ensure
that nothing serious fails that would have been caught by a check.

In the absence of any careful analysis, it is not clear whether it is better
to leave on all checks or not. The important thing is to realize that in the
absence of a careful analysis, turning all checks on is not necessarily
safer than leaving them off.