Re: Reasons why you don't prove your programs are correct

steve@hubcap.clemson.edu ("Steve" Stevenson) writes:


>I'm trying to discover the real reason why people do not prove their programs
>are correct. I would like to collect those reasons --- even those snappy
>one liners that we all use as excuses.


What is your definition of proof? I spent the last year doing honours
computer science as Queensland University, and 2 of my 4 subjects were quite
devoted to the topic of proving programs correct. One was a specification
and design subject - in which I came to the conclusion that any decent sized
program (written in anything approaching a `natural' style) was not worth
the effort, if it was possible. We studied 2 approaches to refining programs
from specifications, both of which allowed a very restricted class of
program to be refined with any ease (and once again I doubt the possiblity
of refining large programs, or programs with interesting data structures.)


The other subject was a functional programming subject, and we attempted a
proof of a simple interactive mastermind program, using fixed point theory.
Here it is also really a process of refining the program to make it easy to
prove - ending up with some drastically warped code (some [unenlightened]
people claim that all functional code is warped.) No one in the class, not
even the most brilliant mathematical minds, managed to get a plauseable
proof, and if they did I contend that it would be of no real assistance
because, to my thinking, a proof's first purpose is to convice someone of
correctness, and a proof-by-intimidation is not really convincing.


Besides this the code you can write for most provable programs is
intollerably dull - no recursion, no dynamic data stuctures, only arrays, or
else you have to prove that you can't blow a stack, or run out of memory.


If you accept testing as a means of `proof' (this does not conform to my
definition), then even that is fraught with problems, how do you choose your
test data, can you test all permuatations (in some cases this is
impossible.)


So in the end it comes down to doing reasonable testing and having a certain
confidence in your code reading ability.
--
keithd@anvil.oz.au
(07)870 4999
Anvil Designs Pty Ltd
PO Box 954, Toowong,
4066, Australia.

Return to the comp.compilers page.
Search the comp.compilers archives again.