steve@hubcap.clemson.edu ("Steve" Stevenson) (01/06/90)
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.
Please forward your comments ( short flames ok) to me by E-mail. I'll post
the replies if there is sufficient interest. Thanks.
--
Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu
Department of Computer Science, (803)656-5880.mabell
Clemson University, Clemson, SC 29634-1906
--
Send compilers articles to compilers@esegue.segue.boston.ma.us
{spdcc | ima | lotus}!esegue. Meta-mail to compilers-request@esegue.
Please send responses to the author of the message, not the poster.keithd@anvil.oz.au (Keith Duddy) (01/17/90)
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. -- Send compilers articles to compilers@esegue.segue.boston.ma.us {spdcc | ima | lotus}!esegue. Meta-mail to compilers-request@esegue. Please send responses to the author of the message, not the poster.
mayer@iuvax.cs.indiana.edu (Mayer Goldberg) (01/18/90)
I don't think that the proof theory which produces boring, unintuitive
yet correct code, is meant for you to use to verify your own programs
... I would think it is meant for automatic code generation. This
could be useful, and time saving.
Mayer Goldberg
mayer@iuvax.cs.indiana.edu
--
Send compilers articles to compilers@esegue.segue.boston.ma.us
{spdcc | ima | lotus}!esegue. Meta-mail to compilers-request@esegue.
Please send responses to the author of the message, not the poster.