Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!tut.cis.ohio-state.edu!zaphod.mps.ohio-state.edu!uwm.edu!ux1.cso.uiuc.edu!ux1.cso.uiuc.edu!m.cs.uiuc.edu!p.cs.uiuc.edu!johnson
From: johnson@p.cs.uiuc.edu
Newsgroups: comp.software-eng
Subject: Re: Some Issues Lying Beneath a Recent
Message-ID: <102100003@p.cs.uiuc.edu>
Date: 28 Feb 90 17:40:07 GMT
References: <3241@umn-d-ub.D.UMN.EDU>
Lines: 74
Nf-ID: #R:umn-d-ub.D.UMN.EDU:3241:p.cs.uiuc.edu:102100003:000:3310
Nf-From: p.cs.uiuc.edu!johnson    Feb 27 14:22:00 1990


>(T1) Formal proofs of program correctness can provide an absolute, con-
>clusive guarantee of program performance;

>(T2) Formal proofs of program correctness can provide only relative, in-
>conclusive evidence concerning program performance.

The problems with these statements is that T1 is not ~T2.
NOTHING provides an absolute, conclusive guarentee of program
performance.  Certainly testing doesn't.  However, words like
"inconclusive" are loaded with hidden meaning, and I don't
want to waste my time doing experiments if I know that they
will be inconclusive.  I want to conclude something!  As a matter
of fact, program verification lets you conclude that your program
does not have dumb coding errors.  Thus, I don't buy either T1 or T2.

>(T3) Formal proofs of program correctness should be the exclusive method-
>ology for assessing software reliability;

>(T4) Formal proofs of program correcness should be the principal method-
>ology for assessing software reliability;

>(T5) Formal proofs of program correctness should be one among various
>methodologies for assessing software reliability.

I don't agree with T3, T4, or T5, either.  Program verification has
nothing to do with assessing software reliability.  Program verification
make your software more reliable, though, but it doesn't help you measure
the reliability, and "assess" means measure to me.


"So it becomes a matter of how confident we need to be that a system will 
perform as it is intended to perform.  We cannot know without testing the
system."

Djikstra: Testing never proves the absence of faults,
          it only shows their presence.

I usually disagree with Djikstra, but this quote of his seems obviously
true.  However, I will counter with a quote of my own

Johnson: If it hasn't been tested then it doesn't work.

Specifications need testing more than anything else.  Prototyping
is a way of testing specifications.  Program verification doesn't
help specifications very much.  Instead, it helps ensure that
the code that you produce matches the specification.  Thus, testing
and verification play complementary roles.

However, there are cases where program verification is much better
than testing at showing that a system behaves as expected.  For
example, a couple of years ago there were some people who were
killed because an X-ray machine emitted much more power than it
should have.  The problem was in supposedly in the user interface;
the operator missed a decimal point or something and specified
too large a number.  People claimed that the user interface should
have caught this.  Maybe, but if I had been building the system and
I had been told that NEVER, under ANY circumstances, should the
machine emit more than X units of power, then I would have found the
one subroutine that turned on power, and written it as

EmitPower(power) {
  if power < X then
      do lots of low level stuff
}

Of course, you would have to test that the low level stuff really
implemented the high level abstraction.  However, after that you
would KNOW that the program would never ask for the fatal power.
Naturally, if the < operation on the computer breaks, then a
patient might still be zapped, but that is a lot less likely than
operator mistake.

Ralph Johnson -- University of Illinois at Urbana-Champaign