📄 proofscantprovetheabsenceofbugs.html
字号:
<head><title>Proofs Cant Prove The Absence Of Bugs</title></head><body><h1><img src="logo.gif"> Proofs Cant Prove The Absence Of Bugs</h1>Perennially we have a little discussion to the effect that <a href="TestsCantProveTheAbsenceOfBugs.html">TestsCantProveTheAbsenceOfBugs</a>. This is a hoary observation probably made by Lady Lovelace, or maybe Grace Hopper, who claimed to have invented the bug. It's true on the face of it: no amount of [blind] testing can be certain to have exercised all combinations of inputs so as to ensure that the program actually works.
<p>The oft-implied idea is that some kind of mathematical proof could in fact "prove" the absence of bugs. The suggestion is that sufficient formal reasoning about the program can determine once and for all that the program is without flaw.
<p>While this may be true in principle, it isn't even somewhat true in practice. The amount of formal reasoning required to prove even the smallest programs is beyond the capacity of most of us. The amount required to prove a payroll, air traffic control system, or telephone switch is literally beyond human comprehension.
<p>Further, human reasoning is quite flawed. It should be obvious to the casual observer that our specialty is not logic. Even the most carefully-crafted mathematical proofs are often erroneous. The typical graduate mathematics homework assignment results in a wide variance of proof quality and correctness.
<p>The issue with regard to bugs is confidence. Defect-finding mechanisms must be applied until human confidence reaches the level appropriate to the impact of an unfound bug. If it's a word processor, you might be less concerned about bugs than if it's a heart-lung machine.
<p>Since confidence is a human feeling, the proof mechanism must be accessible to the person who needs confidence. It may or may not engender confidence in the Vice President to have a wild-eyed mathematician (think Christopher Lloyd as Doc in Back to the Future) assure him "I've proved conclusively that the program will work."
<p>Even if it were true that a formal proof can engender more confidence than conscientious testing, which this author does not believe, the proof approach founders when the program undergoes maintenance. The proof will generally not be revisited under maintenance. When it is revisited, it will generally not be regenerated.
<p>A suite of <a href="UnitTests.html">UnitTests</a> and <a href="FunctionalTests.html">FunctionalTests</a>, on the other hand, survives and can be run, daily even, checking and rechecking each change.
<p>Do the math: <em>Nothing</em> can truly prove the absence of bugs. The usual approach of big-bang testing under a time limit and pressure to release is clearly bad. A comprehensive repeatable test suite is much much better. If you're not doing <a href="PairProgramming.html">PairProgramming</a> (and perhaps even if you are), consider doing intensive code reviews (and translating the results to tests). If you're dealing with life and death, consider proving some key algorithms. But in the real world, <a href="YouArentGonnaNeedIt.html">YouArentGonnaNeedIt</a>. --<a href="RonJeffries.html">RonJeffries</a>
<hr>
Are there any wikizens actually using program proof in their day-to-day work? Please tell us about it.
<p>Are there other techniques that you actually use? Please report on those as well.
<hr>
A static type-checker is a poor man's program prover. I recently did a big refactoring in a C++ program, and the type system gave me a lot of confidence that the change was correct. The type-checker is run automatically; the type system necessarily keep in sync with the program.
<p>I'm not arguing against testing, just saying that proofs can have a role. -- <a href="http://c2.com/cgi/wiki?DaveHarris">DaveHarris</a>
<hr>
See <a href="http://c2.com/cgi/wiki?ProofOfCorrectness">ProofOfCorrectness</a> for a couple of additional comments.
<hr>
<em>Further, human reasoning is quite flawed. It should be obvious to the casual observer that our specialty is not logic. Even the most carefully-crafted mathematical proofs are often erroneous. The typical graduate mathematics homework assignment results in a wide variance of proof quality and correctness.</em>
<p>Actually, there is a way around the unreliability. If you define a formal language for proofs you can check mechanically whether something is really a proof. You still have to come up with the proof of course. In a way this is similar to automated unit tests. You do have to write them, but once you have them you can check them automatically.
<p>(Actually it would take an enormous amount of work to write something like ZermeloFraenkelUnit<a href="http://c2.com/cgi/wiki?edit=ZermeloFraenkelUnit">?</a> even for Smalltalk, but it can be done. And I guess that someday it will be done.)
<p>The drawback of unit tests is that they cannot be absolutely complete. Formal specifications can be absolutely complete. Of course the drawback of writing proofs is that it takes a lot more time than writing code and that it interferes with the rapid feedback loops of XP. But if we ever develop AI that is smart enough to do most of the work it could become much more practical.
<p>I said that formal specifications can be absolutely complete. That's not really true, because in the end you cannot definitively prove anything about the real world. But if you give a precise syntax and semantics of your programming language and your proof language you can prove that a program conforms to a specification.
<p>But, as Ron says, for most applications <a href="YouArentGonnaNeedIt.html">YouArentGonnaNeedIt</a>. And I think that even for applications that need to be ultra-reliable and might benefit from proofs you wouldn't start with a formal specification. As long as our AI isn't smart enough to help us come up with a proof-code combination from a specification more quickly then we can find them with programming and unit tests, unit tests would still be the tool that we use to come up with a nearly correct program. Once you have a nearly correct program you can use the formal methods to fix the few remaining bugs.
<p>Actually, this is a bit of a hobby horse of mine. Synthesis isn't analysis. Writing programs and writing proofs requires creativity, trial and error, handwaving and sometimes thinking the illogical. Analysis proceeds deductively, synthesis proceeds inductively. You don't start with a neat Z-specification and then arrive at a hundred thousand lines of C++ code by stepwise refinement. You arrive at those one hundred thousand lines of C++ (or ten thousand lines of Smalltalk ;-)) by <a href="ExtremeProgramming.html">ExtremeProgramming</a>. Afterwards you can use formal methods to come up with a neat stepwise refinement. Stepwise refinement is great for checking stuff. It's useless for finding stuff.
<p>I'll get off my soap box now ;-)
<p><a href="http://c2.com/cgi/wiki?MartijnMeijering">MartijnMeijering</a>
<hr>
Please correct me if I'm wrong, but as I understand it the end of a formal proof of correctness is really a statement that two expressions, the specification and the program, are equivalent. But there is no guarantee that the specification is what it SHOULD be. There is still an element of human judgement involved, even with automated theorem proving. --<a href="KentBeck.html">KentBeck</a>
<p>You're absolutely right. We can't prove more than conformance to specification. And even that is an idealisation, because ultimately a system runs on real hardware in the real world and we mere mortals can't definitively prove things about the real world. And of course, as you say, we have no guarantee that the specification is what it should be. We can ask bright minds to review it, we can test it, but we cannot prove it's right. So we must not delude ourselves about the possibilities of formal proofs.
<p>We also mustn't delude ourselves about the need for proofs. A structural engineer can't prove mathematically that his bridge or skyscraper or whatever won't fall down. But they don't fall down terribly often, unless people start dropping bombs on them. Boeing can't prove the "correctness" of their planes. And yet we consider them safe enough to risk our lives flying in them.
<p>Also, right now formal methods aren't practical. We just don't have the technical and mathematical framework for doing it. You have to give a mathematically precise definition of both the syntax and semantics of your programming language and your proof language. This definition is going to be rather long, so you'll probably have to define at least one level of metalanguage first. You also have to come up with a sound set of inference rules. (And what do you take? Classical logic, intuitionistic logic?, some other "non-standard" logic?).
<p>Then, in order for this to be practical, you need a program that verifies proofs. Of course, that program needs to be correct. You could try to prove it correct with itself. But that doesn't prove anything. That's more like a unit test. So, you'd check it by hand as well. Or you'd build more than one implementation and let them check each other. You could ask the brightest mathematicians in the world to try and find mistakes in the proofs. You could offer a million dollars for someone who finds a mistake.
<p>Also, you need to prove that the compiler that compiles your proof-program conforms to its specification. You need to prove that the processor you run the program on conforms to its specification. And that is about as far as you can go.
<p>Obviously, this is an enormous amount of work, but I think it is doable. And I think that someday someone will do it.
<p>But despite these limitations, I still find the idea appealing. If someone ever builds ZermeloFraenkelUnit<a href="http://c2.com/cgi/wiki?edit=ZermeloFraenkelUnit">?</a>, I think it could be very useful. Suppose we could cost-effectively (for a small number of critical applications) prove that a program conforms to its specification. Wouldn't that be a tremendous archievement? Wouldn't that give you a lot of confidence in the correctness of a program? Once it becomes doable, wouldn't we want the control software for a nuclear plant to be "proved" correct? Software has the potential of being the most reliable technology in the history of the world. --Martijn
<p>Interesting that you point out the need to prove the automated prover and the compiler and the processor. <a href="UnitTests.html">UnitTests</a> provide verification for all aspects of the system they run on.
<p>It should also be noted that there is less than complete agreement on what constitutes a mathematical proof. Will ZermeloFraenkelUnit<a href="http://c2.com/cgi/wiki?edit=ZermeloFraenkelUnit">?</a> satisfy Constructivists? --<a href="http://c2.com/cgi/wiki?KielHodges">KielHodges</a>
<p><hr>
To quote <a href="http://c2.com/cgi/wiki?DonaldKnuth">DonaldKnuth</a>, "Beware of bugs in the above code; I have only proved it correct, not tried it." (<a href="http://www-cs-faculty.stanford.edu/~knuth/faq.html">http://www-cs-faculty.stanford.edu/~knuth/faq.html</a>)
<p><hr>
<em>Are there any wikizens actually using program proof in their day-to-day work? Please tell us about it</em>
<p><em>Of course the drawback of writing proofs is that it takes a lot more time than writing code and that it interferes with the rapid feedback loops of XP</em>
<p>Well, I'm not doing every-day proofs right now, but we are definitely looking at doing so in the very near future, because its quicker, easier and more iterative than writing tedious unit tests. We already use formal proofs as a part of our
final release procedure.
<p>OK, I'll come clean. I'm not talking about software. My field is microprocessor
core design (<a href="http://c2.com/cgi/wiki?TriCore">TriCore</a>). The formal methods we use for releases ("tape out") are
of 2 types: formal equivalence and static timing analysis. (You could argue
that STA is not a formal proof: simply a static verification technique).
<p>We do a formal equivalence check between a highish level (RTL) description
and its gate level equivalent. This is possible becuase the RTL is written
using a "synthesisable subset" of hardware description languages. Its simply
a matter of comparing the combinatorial logic between sequential elements,
which is well within the scope of today's tools.
<p>Modern tools are now going beyond equivalence checking into the realm of
"property checking". Their notations are migrating from obscure mathematics towards user friendly languages that are readable to average programmers
(This means a Verilog-like syntax, which is similar to C).
<p>One of the problems with verification of complex hardware designs is the
cost of unit tests for entities whose interfaces are not fixed in stone.
Verification requires testbenches to attach stimuli to a design, test
patterns to stimulate it, and oracles to determine the expected outputs.
Where XP assumes that the cost of migrating tests during refactoring is
small, the cost of doing so in hardware is prohibative.
<p>Enter property checking. "Properties" are simple expressions that define
a true statement about a design. For example, "the output will be asserted
if, on previous clock cycles, the input sequence was 1,2,3,4" (this assertion would, of course, be expressed in an appropriate language). The hardware designer (or pair of designers) can write this assertion in seconds, and it can be automatically checked repeatedly by tools. Even more important, the assertion can easily be strengthened to "the output will *only* be asserted if ..." -- this is not more expensive to check using formal proofs, but the cost of checking it through dynamic simulation is very high (could take hours, days,
centuries of CPU time).
<p>In summary, where XP uses unit tests to enable iterative development, hardware
design is moving towards formal proofs. They are much cheaper and more flexible than unit tests.
<p>--<a href="http://c2.com/cgi/wiki?DaveWhipp">DaveWhipp</a><hr><a href="http://c2.com/cgi/wiki?edit=ProofsCantProveTheAbsenceOfBugs">EditText</a> of this page (last edited July 5, 2000)<br><a href="http://c2.com/cgi/wiki?FindPage&value=ProofsCantProveTheAbsenceOfBugs">FindPage</a> by browsing or searching<p><font color=gray size=-1>This page mirrored in <a href="index.html">ExtremeProgrammingRoadmap</a> as of March 31, 2001</font></body>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -