Royal Pain

[Henry Spencer]

On Fri, 18 Jun 2004, Lennart Sorensen wrote:
> > And of course, it's impossible to prove there are no bugs.  You can only 
> > fail to find some.
> 
> That is actually not true.  If you have a well defined specification of
> what the behaviour of each piece of the program must be for specific
> inputs, you can actually prove the behaviour of each part of the program
> correct...

Unfortunately, this assumes that the *proofs* do not have bugs.  Which, in
fact, program proofs-of-correctness often do.  There was an embarrassing
paper a number of years ago which took a careful look at published
correctness proofs in the computer-science literature, and found bugs in
many of the "proven correct" programs.  This was particularly noteworthy
because most of those programs were quite small and simple ones, to keep
the size and complexity of proofs down to something that could reasonably
be published in a paper. 

Correctness proofs have their uses -- in particular, *attempting* a proof
is a powerful bug-finding method -- but they are far from infallible.

                                                          Henry Spencer
                                                       henry-lqW1N6Cllo0sV2N9l4h3zg at public.gmane.org

--
The Toronto Linux Users Group.      Meetings: http://tlug.ss.org
TLUG requests: Linux topics, No HTML, wrap text below 80 columns
How to UNSUBSCRIBE: http://tlug.ss.org/subscribe.shtml