Re: Software Safety (was: Need help with PowerPC/Ada and realtime tasking)

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

"I agree.  About a decade ago, at workshop on formal verification of Ada
programs, I got into a heated argument with David Gries about a useful
definition of correctness.  I argued that it was useless to prove a
program conformant to formal specifications unless one had a high degree
of confidence that the specifications expressed the customer's intent.
Gries seemed to have in mind a model whereby the customer presents the
software developer with a contract expressed in the form of formal
specifications; if the software developer conforms to the specifications,
he has fulfilled the contract, even if the customer doesn't get what he
really wanted.
"

I certainly agree that it is unfortunate that the term correct has been
hijacked, however, it is tilting at windmills to try to change this now
(sort of like my efforts to prevent the misuse of moot and oxymoron :-)

Your "heated argument" reminds me of a conference I was at where Niklaus
Wirth was talking about programming being a process of refinement whre
the one and only issue was that refinement should be correctness preserving.

At the end of the panel session, I commented that the whole notion of 
correctness is misguided, because the issue is building reliable software,
not correct software. I used as an anology car manufacture, car companies
are interested in building reliable cars, almost no one would talk about
a correct car. And indeed almost any car does NOT meet its specifications,
but the issue is whether the defect are minor. A small area of miscolered
paint under the rear bumper renders a car incorrect, but not unreliable!

In the case of softare, correct and reliable are of course NOT the same.
Reliability includes the specificatoin being correct, and of course
we have no way of proving a specification correct, at most we could
prove it consistent, but that might simply mean it is consistently wrong!
Actually as specifications get more formal, it often gets harder and harder
to determine if it is correct. Try looking at the formal definition done
by the EEC for Ada 83, it is two fat telephone books of mathematical
formula -- and there is no way of ensuring it is correct [in fact, as
would be expected for what is essentially a huge program that has never
been run, it is not correct].

On the other hand, a program that trivially departs from its spec (background
of the GUI is slightly different shade of green than specified for example)
may still be completely reliable even though it is not correct.

So I prefer to leave the term correctness to (mis)mean what David Gries and
Niklaus Wirth (and many others) insist on, and simply to recognize that it is
not the most important property, and if I am a customer I want a program
that works, a correct (in this sense) program that does not work is of
no interest to me, and I will not sign a contract that says that all the
program has to do is to implement correctly some formal specification!

P.S. At that panel session, when I made the comment about cars not having
to be correct, the audience, quite frustrated I think with the panel
presentation, applauded the comment loudly :-)