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

[ncohen@watson.ibm.com (Norman H. Cohen)]

In article <DsFM3B.CqB@world.std.com>, bobduff@world.std.com (Robert A
Duff) writes: 

|> The reason I object to "correct" is that I've seen many cases where
|> people misunderstand the term.  Even people who ought to know better.

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've seen arguments along these lines: "I proved so-and-so program
|> correct.  Therefore, it obviously can't have any bugs, or do anything
|> wrong.  Therefore, there's no need to test it."  A bogus argument, but
|> it's easy to fool people with that sort of argument, because "correct"
|> really does mean "good" or "perfect" in plain English.

And yet there have been studies analyzing the causes of software "errors"
and attributing roughly half of them to mistakes in the specifications!

--
Norman H. Cohen    ncohen@watson.ibm.com