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

keithd@anvil.oz.au (Keith Duddy)
12 Jan 90 05:08:13 GMT

          From comp.compilers

Related articles
Reasons why you don't prove your programs are correct steve@hubcap.clemson.edu (1990-01-05)
Re: Reasons why you don't prove your programs are correct keithd@anvil.oz.au (1990-01-12)
Re: Reasons why you don't prove your programs are correct mayer@iuvax.cs.indiana.edu (Mayer Goldberg) (1990-01-17)
Re: Reasons why you don't prove your programs are correct pardo@cs.washington.edu (1990-01-22)
Re: Reasons why you don't prove your programs are correct pardo@cs.washington.edu (1990-01-24)
Re: Reasons why you don't prove your programs are correct gateley@m2.csc.ti.com (1990-01-26)
| List of all articles for this month |

From: keithd@anvil.oz.au (Keith Duddy)
Newsgroups: comp.compilers,comp.edu
Date: 12 Jan 90 05:08:13 GMT
References: <7578@hubcap.clemson.edu>
Organization: Anvil Designs Pty Ltd, Brisbane, Australia

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.





Post a followup to this message

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