Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!ncar!noao!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions and other fantasies
Message-ID: <2216@optima.cs.arizona.edu>
Date: 20 Apr 91 06:45:35 GMT
Sender: news@cs.arizona.edu
Lines: 59

Oops.  The sentence above is true enough, but it isn't what I intended
to say.  I meant to say that "You don't know anything more about
whether the program's behavior is correct by the real-world
specification."

]You know the same thing after a formal proof that you do after running a test
]suite:  if there were errors (failed proof, failed tests) then you have some
]bugs to fix; if there were no errors (proof checked, all tests passed) then
]you know that the program behavior agrees with (a) the behavior specified by
]the specification, or (b) the behavior represented by the test suite.

You have missed the entire point of the article: the behavior
specified by the specification may bear no relation to the correct
behavior for the program.  Thus knowing about the formally specified
behavior does not tell you about the correctness of the behavior.  I'm
talking about what you _know_ in the sense of mathematical certainty.

It has been said that mathematics gets its certainty by not actually
saying what it is talking about.  A proof of corrrectness is only a
"proof" if it is applied to a formal specification with no relation to
the real world.  Once the specification is applied to the real world,
you lose certainty.

The reason I bring this up is because some people on this newsgroup
have been talking like formal verification is some sort of magic that
actually proves that a program does what it is supposed to do, and
that testing is an unreliable hack.  Quite the contrary, testing is
now and always will be essential.  Formal verification is now and
always will be a special technique that is only useful in certain
kinds of applications, and always in conjunction with testing.  No,
testing does not give mathematical certainty.  There is no such thing
in the real world.

I can write a program that satisfies the following specification of a
sort program:

  Forall 0 < i < N . Output[i-1] <= Output[i]

and prove it correct even though it does not work correctly for any
real world example.  Since the specification is incorrect, the proof
tells nothing about how the program is related to the real world.  All
a proof of correctness does is relate one formal specification to
another.  It doesn't tell you that either one is correct.

Disclaimer: Nothing in the above should be taken as an assertion that
program verification has no value.  It is only intended to clarify
exactly what is (and is not) mathematically proven by a formal proof
of correctness.  Furthermore, the author loves dogs and small children
and is not a lunatic who just likes to drop bombs in comp.lang.misc
and watch the fireworks.  Really.

No, I mean it.  I didn't even want to talk about program verification,
I was provoked.

OK, I could have ignored it, but... never mind.
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman