comp.lang.ada
 help / color / mirror / Atom feed
* correctness vs liability
@ 1997-08-25  0:00 Robert Dewar
  1997-08-25  0:00 ` Robert Dewar
  0 siblings, 1 reply; 2+ messages in thread
From: Robert Dewar @ 1997-08-25  0:00 UTC (permalink / raw)



Robert said:

<< No, I disagree, these are completely different qualities, they are
   related, but as I said earlier, you can have reliable programs that
   are not correct, and correct programs that are not realiable.>>

Jeff replied

<<This is a nonsensical statement. In the first case, you will have a
  program that reliably does the *wrong* thing, and in the second case,
  you will have a program that doesn't do the right thing all the time.
  Neither of these cases is of any interest to the goal of creating
  high quality functioning software.>>


Yes, I know it is easy to react like that, but actually for me, the
ability to understand that Jeff's reply is itself nonsense is one of
the critical perceptions that programmers need to gain from experience.

The point is that correctness can only be defined in terms of equivalence
between an implementation and a formal specification of what the program
is expected to do. It is thus simply a self-consistency measure.

How can one have realiable programs that are not correct? Very simple,
and in fact, I would guess that virtually all large realiable programs
in the world fall into this category. The point is that a program can
be realiable if it has a very long mean time between catastrophic

failures, and it can also be reliable even if it has some very minor
discrepancies from its spec that simply don't matter. As an example
of the latter, I quote from an experience one of my students had in
a summer job for a large publisher. He found that their main mailing
list update program, which was used to update a list of about seven
million names, lost a few names at the start of the file every year
when it was run. He proposed to modify the program to fix this. His
boss was furious "Don't touch that program, it is one of the most
reliable programs we have around, yes, we know it loses a couple of
names, but hundreds of thousands of those names are junk anyway,
and losing a couple is unimportant." Now I suppose you can say that
a really accurate spec would allow such a loss of names, but such
specs are pretty difficult to imagine.

Basically we expect any large program to contain flaws and defects, and
thus to be imperfect, and thus incorrect, but that does not stop it from
being reliable. After all consider the analogy with cars, we often see
something in a review of a new car which reads "this is one of the most
reliable cars around, there were only three defects on delivery, all minor."

If you really think realiability requires correctness, then you are saying
that it is impossible to write large reliable programs, which is nonsense.

As for the other possibility, correct programs that are unreliable. This
most often occurs because the specification did not anticipate some
situation which happens in practice and causes unreliable operation. Sure
the spec is wrong in this case, but correctness, if it means anything,
means consistency with the spec you have. There is obviously no way of
proving that a spec is correct (chase this back like the Tortoise does
to Achilles after the race if you like :-)

So if your meaning of correctness is that the spec has to be provably
correct, then it is not a useful concept. In real life, it often occurs
that a customer agrees on a specification, and the program follows it,
but it turns out that the spec is incomplete or wrong. The resulting
program may be correct from some contractual point of view, but if it
is causing the customers baggage delivery system to fail, then it is
by no reasonable measure, a realiable program.

Yes, in school, one is often taught a naive model in which reliability
and correctness *are* synonymous, but real life is not like that!

Robert Dewar





^ permalink raw reply	[flat|nested] 2+ messages in thread

end of thread, other threads:[~1997-08-25  0:00 UTC | newest]

Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
1997-08-25  0:00 correctness vs liability Robert Dewar
1997-08-25  0:00 ` Robert Dewar

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox