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

[bobduff@world.std.com (Robert A Duff)]

In article <dewar.834237518@schonberg>, Robert Dewar <dewar@cs.nyu.edu> wrote:
>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 :-)

You tilt at "moot" and "oxymoron".  I tilt at "correct".  We all have
our pet peeves, I suppose.  If we think we can actually *change* any
such usage, we're either prophets or deranged (usually the latter).

;-)

Natural language changes, not always for the better.

>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!

Indeed.

>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].

There are two things at work here: (1) as one gets more formal, one gets
a deeper understanding, and eliminates bugs, and (2) as one gets more
formal, one gets further removed from the intuitive notion of what the
software really ought to do, and this causes bugs.

>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.

True, but you have to admit that this is less important than the other
way 'round, where software obeys its spec but does some damage.  I will
tolerate when somebody *insists* on the correct shade of green, if they
also insist on things that really *do* matter.

And one shouldn't forget that about half of the bugs really are the kind
of "plain old bugs" where the software doesn't do what the spec says it
should, and the spec is, in fact, right, and everybody agrees it's a
bug.

- Bob