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

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

Bob Duff said (if I have not lost track of who said what :-)

"> I suppose it depends on your definition of "correct".  The
> proof-of-correctness folks define "correct" to mean "correctly obeys the
> formal specification".  To me, that's a bogus definition.  In plain
> English, a "correct" program is one that does what it's supposed to do,
> regardless of whether the specification is wrong.  If you show me a word
> processor that deletes my file when I told it to italicize a word, to
> me, that's incorrect, even if you can show me a (bogus) formal spec that
> says that the "italicize word" function should delete files.  If you
> show me a flight-control program that crashes airplanes, that's
> incorrect IMHO, despite the fact that you might show me a formal spec
> saying it did what the formal spec says."

What's the point of degrading this useful technical term this way. By
your definition, correct just means good or some such subjective term.
The concept of obeying a formal specification is a useful one, and it
is one which has been given the name "correctness" in the programming
language area.

I admit is occasionally confusing when standard English words are (mis)used
in a specific technical way, but as long as everyone understands the
usage (and correctness has been used in this specific way for many years),m
then it is useful (after all the Ada 95 RM is full of normal English words
used in a non-standard way :-)