6 Jan 89 22:17:01 GMT

Related articles |
---|

Automatic Proofs (WAS: Why Can't We Build a C Compiler?) pardo@june.cs.washington.edu (1989-01-06) |

From: | pardo@june.cs.washington.edu (David Keppel) |

Newsgroups: | comp.compilers |

Summary: | long |

Date: | 6 Jan 89 22:17:01 GMT |

References: | <3112@ima.ima.isc.com> <3134@ima.ima.isc.com> |

Organization: | U of Washington, Computer Science, Seattle |

unido!gmdzi!jc@uunet.uu.net (Juergen Christoffel) writes:

*>[How do you prove the prover? (e..g, how can we*

*> be confident that the prover is itself correct)]*

Several answers:

* If the prover proves an arbitrary specification, then we prove the

prover trivially once we've built it. Consider a C compiler that is

written in C and which illustrates the programs that it compiles.

(An illustrated program is one that shows you graphical views on the

internal data structures of the program. Better descriptions and

references on requests). Once we have an illustrating compiler, it

is trivial for the compiler to illustrate itself.

* ``Perfect'' proofs are not necessary if the prover tells us what it

*didn't* do. Thus, the prover need not be complete. (This view may

be unpopular with some. By analogy, I believe that a compiler

should do what it does very well and that it is ok if I have to

write context-swap code by hand). If we could automatically prove

that certain parts of a program are correct, then we are still ahead

of where we are right now. Things that are especially important to

get correct will be written so that they are more amenable to a

prover. It *is* important for the prover to identify those things

that it can't prove.

* Confidence through repeated use: even if parts of the prover remain

unproven, there is a measure of confidence in the result, since the

prover has been used ("successfully") to prove some number of other

programs. Good code that the prover ``proves'' wrong will be

detected fairly easily. Bad code that isn't proven incorrect will

be harder to track down, since we may have to wait until a

``proven'' program crashes to identify something that the prover

didn't get right.

The moderator writes:

*>[Based on other standards, I'm skeptical that any non-trivial program*

*> could have a bug-free specification, given current formalisms.]*

Put another way, a perfect prover shows that the specification and the

code match, but doesn't show that the program is *correct*.

Agreed. But there is a lot that *is* amenable to proof. Consider a

common argument for using HLLs: ``The complexity of most code is best

managed by machine. Spend 90% of your time worrying manually about the

10% of the code that is most important, let the compiler take care of

the rest''. This same kind of argument can be applied to proofs.

If I want to prove that my sort routine is stable, then I need to prove

that it is a sort and that the sort is stable. It might be easy for

me to state formally that the results are sorted and have my prover

show that it is a sort. It might be that (for some reason) the prover

can't show that my sort is stable. That's still better than forcing

me to do it *all* by hand, since the part that is ``hard'' to me may

be ``easy'' for the machine. Also, I'll have more confidence in the

proof by the machine than in my own (hand) proof, since humans make

bugs in proofs much as they make bugs in the code they're trying to

prove. (Thanks to Richard Fateman for pointing this ``obvious'' fact

out for me.)

Finally, to use another compilers argument, ``Focus on clarity. As

the optimizer matures, the machine-generated optimizations will get

closer and closer to the hand-optimized version.'' As the prover

gains maturity, less and less of a program will need to be proven by

hand (or, alternatively, more and more of the program will be proven

correct).

;-D on ( Proof by two legs ) Pardo

--

pardo@cs.washington.edu

{rutgers,cornell,ucsd,ubc-cs,tektronix}!uw-beaver!june!pardo

--

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.