Re: Safety-critical development in Ada and Eiffel

[dewar@merv.cs.nyu.edu (Robert Dewar)]

Nick writes

<<> OK, so if you can't write such requirements in a rigorous way, how can
> you write the application. If you can write an application that meets
> the requirements, you can write a coded spec for the problem. In the
> extreme case, the code for the application is the specification.>>


Many people have made statements like this, but in my experience, this is
quite false. It is often the case that it is impossible to write down
requirements in a rigorous way, either because you don't know what they
are, or they are stated at a level of abstraction ("use a pleasing color
scheme, easy on the eyes, for the GUI") that is not susceptible to
formalization.

Sure, the code for the application is *a* specification of *something*, but
most likely it is *not* *the* desired specification.

This is often frustrating to those who want a nice clean theoretical
model that guarantees reliable code, but we need methods that can indeed
handle the more general case where we do not always have rigorous
specifications.

Note that the problem of not being able to create such specifications
is not restricted to hardware. Consider the two requirements that
were placed on the IBM Trackpoint before its release:

(a) On average, people must find it as easy to use out of the box as a
trackball, even if they have experience with a trackball.

(b) On average, people must find the trackpoint as easy to use as a mouse
given extensive practice with both.

These were taken very seriously, and the release of the product was
delayed until these requirements were met. But I don't see how you
could formalize these requirements into a form that would rigorously
tell you if your mechanical device met these requirements.

Once I heard Wirth state that one should simply refuse to attempt to
write a program in such circumstances. His point was that it was impossible
to guarantee correctness by the method he was proposing at the time 
(successive refinement, maintaining the invariant of correctness).
My response (that what we needed was reliability, not correctness, and
that correctness was only a tool to achieve reoliability), drew applause
from the audience, which was frustrated by this narrow view.

Things are not as simple as one might hope :-)