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 st...@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906 -- Steve (really "D. E.") Stevenson st...@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906
In article <16520...@hpisod2.HP.COM> de...@hpisod2.HP.COM (Dave Decot) writes: >Theorem provers are too slow and expensive.
Theorem provers might be slow and expensive, but program provers are not available at any seed or price. Indeed it is doubtful that such programs can be written at all. (See the CACM article entitled " Program Verification: The Very Idea". I can no longer remember the exact CACM it was in, sorry. My best guess would be Sept. 1986 or 1989.)
>Programmers are too lazy to write assertions and invariants, especially >for complex code (which if they weren't lazy wouldn't be so complex).
As was discussed in another new group (comp.ai or comp.object), assertions have little to do with proving a program correct. The best they can do is prove that the assertions are met. While this is a good thing, it does not PROVE anything. How do you prove that the assertions assert anything useful?
Blaming the programmers is a cheap shot. If that were the only problem, then some programs would be proven correct, the fact almost no commercial or military programs have ever been proven correct suggests that the technology is not available. Remeber that assertions are not nearly enough.
Dave Decot makes it sound like there is a choice. You can choose to prove your program correct, or not prove it correct, but this is false. With current technology you can not prove a (real-world) program correct.
Joshua Levy -------- Quote: "If you haven't ported your program, it's not Addresses: a portable program. No exceptions." jos...@atherton.com {decwrl|sun|hpda}!athertn!joshua work:(408)734-9822 home:(415)968-3718
In article <16...@joshua.athertn.Atherton.COM> jos...@athertn.Atherton.COM (Flame Bait) writes:
Theorem provers might be slow and expensive, but program provers are not available at any seed or price. Indeed it is doubtful that such programs can be written at all. (See the CACM article entitled " Program Verification: The Very Idea". I can no longer remember the exact CACM it was in, sorry. My best guess would be Sept. 1986 or 1989.)
This article is only of interest because of the resulting CACM Flame-Fest that ensued. The article itself merely makes the obvious statement that a program-proof is wrt some set of axioms about the behaviour of the hardware that the program runs on. The article's author then concludes that you "cannot prove programs correct" because the hardware may not satisfy the axioms. Personally, I would be very happy with a program that would only malfunction if the hardware adds 1+1 and comes up with 3.
What the author (and apparently the poster) fails to realize is that the purpose of a program proof in the real world is to increase your confidence that the program will do what you want it to do. Sure, some academics with axes to grind (and grants to obtain, and tenure to achieve) indulge in some faulty advertising, but anyone seriously working in the area is aware that a proven program can still fail to do what the user wants it to do.
Of course the hardware axioms could be unsatisfied, the proof itself could be faulty, a faulty compiler could be used, etc., but that does not eliminate the fact that a program proof increases your confidence that the program does what you want it to do.
As was discussed in another new group (comp.ai or comp.object), assertions have little to do with proving a program correct. The best they can do is prove that the assertions are met. While this is a good thing, it does not PROVE anything. How do you prove that the assertions assert anything useful?
This comment applies to any technique that can be used to increase your confidence in a program, and is totally pointless. To repeat, the point of a program proof is to increase your confidence that the program does what you want. Neither it, nor any other technique will guarantee it. Sometimes testing is better, sometimes code walkthroughs, usually a combination of all the various techniques is best.
I resisted answering this for a long time, except by mail, but now I just can't resist any longer.
I can't answer the question "why I don't prove my programs correct" because I do. All the time. As a matter of course. Almost without exception.
As a practical matter, the issues Fetzer raised in his diatribe passing falsely as a technical article can be largely ignored, both from the standpoint of engineering and mathematically. You simply must know where to draw the line. You assert a semantics for whatever you can't prove, assume that as part of your theorey, and proceed. when you realize your code, you firewall the parts which are assumed but unproven with assertions that are executed at run time, and ensure that the semantics you assumed are the semantics you got. Thus as a matter of engineering, Fetzer's Dilemma -- which we might state as "how can mathematics which is deductive apply to the real world, about which we can only gather data and validate hypotheses?" -- can be (almost) ignored. All the issues raised are issues that apply equally to other pure vs. applied mathematics dichotomies; all must be handled by the (implicit or explicit) assumtion that our physical models are a sufficiently good approximation of the "unspeakable" real world.
But, in fact, these issues had been examined at some length in the formal methods community. Had Dr Fetzer been conversant with the literature, he would have known it; had the reviewers been appropriately chosen, they would have called him on it. The fact that Dr Fetzer's article was published without appropriate examination of the literature is failure on the part of CACM which I think is very hard to excuse.
*On the other hand*, Fetzer's Dilemma does expose an unfortunate tendency in some parts of the formal methods community that we might term "Hoare's Folly." Tony Hoare has said in print that proven programs remove the need to debug *and to test*. For the reasons that Fetzer described, this is clearly untrue. You don't know the way the apple tastes until you taste the apple. The program as a mathematical construct can be proven; the realized program as a physical construct -- a sequence of executable operations in a physical memory and their execution in a physical processor -- can AND MUST be tested.
It is a myth that programs must be verified by theorem provers to be proven. Hand proofs can be done; in several small experiments I have seen very large improvements in quality as measured by number of defects seen per thousand lines of code (I know, I know, but propose a better measure and I'll use it.) These are only slightly better than pure anechdotes; I am currently looking for research funding to perform experiments which would more strongly confirm the hypothesis.
It is a fact that many of the clients or customers for very highly trusted programs require verification using a mechanical prover or proof checker. I am willing to work with one when it is required, but there is as yet little evidence that they provide more certainty than hand proofs, and hand proofs are lots cheaper. I can't help but think that the use of theorem provers in this context is often a case of the old myth that if it's been blessed by a machine, it is somehow ennobled and incapable of error.
(I'm not claiming that theorem provers are useless, either. There are contexts in which they can be very useful. There is ongoing research which will help to delimit these contexts. We need to know more about it.)
Program proving isn't a panacea: among other things, a proof doesn' t tell us a damned thing about the suitability of the requirements to the user's needs. I don't see how formal methods can help much with that question, but there is a lot of "requirements engineering" literature that I should read before I have an informed opinion.
Pant, pant.
These are, of course, only my opinions. They are not necessarily held by Duke University, the Department of Computer Science, or any of my consulting clients, and would probably be bitterly contested by some subset of the above. Charlie Martin (c...@cs.duke.edu,mcnc!duke!crm)
In article <16...@joshua.athertn.Atherton.COM> jos...@athertn.Atherton.COM (Flame Bait) writes:
Theorem provers might be slow and expensive, but program provers are not available at any seed or price. Indeed it is doubtful that such programs can be written at all. (See the CACM article entitled " Program Verification: The Very Idea". I can no longer remember the exact CACM it was in, sorry. My best guess would be Sept. 1986 or 1989.)
Could someone post the exact reference, please ?
Periklis Tsahageas Software Eng. IV Imperial College, London
In article <16...@joshua.athertn.Atherton.COM>, jos...@athertn.Atherton.COM (Flame Bait) writes:
> With current technology you can not prove a (real-world) program correct.
In my corner of the real world, most programs consist mainly of operating system and other outside vendor supplied subsystem calls glued together with rather trivial computations. It seems to me that it is futile to attempt to prove my programs correct if the low level operations (from my point of view) are not rigorously defined (let alone proven to be correct themselves).
In article <16...@duke.cs.duke.edu> c...@romeo.UUCP (Charlie Martin) writes: >But, in fact, these issues had been examined at some length in the >formal methods community. Had Dr Fetzer been conversant with the >literature, he would have known it; had the reviewers been >appropriately chosen, they would have called him on it. The fact that >Dr Fetzer's article was published without appropriate examination of >the literature is failure on the part of CACM which I think is very >hard to excuse.
Well, I don't excuse it. Has anyone noticed the dumbing down of CACM in order to try to get a broader membership? Long gone are the days when you could find mainly articles like "On the Probability Distribution of the Values of Binary Trees", "Application of Game Tree Searching Techniques to Sequential Pattern Recognition", and "Complex Interval Arithmetic" (these titles taken from random from CACM, Vol. 14, No. 2, Feb. '71 - and, BTW, the sixties issues were even better).
Instead we get whole issues devoted to "Computers and Society", which although an important subject, is not one which can be very usefully applied to most Comp. Sci. professionals (although we build the tools, we often have little say in usage policy). The inclusion of more "practicum" articles rather than research is another sign of decline. And the final nail in the coffin has been the recent inclusion of a Personal Computing column. Any "technical" magazine which allows one of these rotten apples into its pages has never stayed "technical" long. I don't know if it's because the editorial policy has shifted before the column appears or if it's just some sort of karmic influence. However, I still believe that before long we will be seeing articles on "How I Used Lotus 1-2-3 to do a Least-Squares Analysis" or others of its ilk (after all, we do have to increase membership, eh?).
All in all, I wish that I could drop the $30 charge for CACM and keep my membership for Computing Surveys, ToPLAS, SIGArch, SIGPLAN, etc. However, ACM will not allow me to do this. It is becoming more and more obvious to me that CACM is becoming more of an embarrassment than a flagship publication. Maybe it's just that I'm grumpy today. Has anyone else noticed this, or am I just getting continually more grouchy as the years go along? --
Frank A. Adrian Mentor Graphics, Inc. fra...@mntgfx.com
>/ c...@romeo.cs.duke.edu (Charlie Martin) / 12:11 pm Jan 20, 1990 / >I can't answer the question "why I don't prove my programs correct" >because I do. All the time. As a matter of course. Almost without >exception.
I've been trying to follow this string, remembering those days in college when the instructor indicated that program proof of correctness was possible, but intractable. Now someone claims to do it. Apparently, often.
o- Do you use a program or tool to do it? o- How complex a program are we talking about? o- If a tool is used, how would I go about acquiring it? If a tool isn't used, what literature (books, articles, or pamphlets) is available to the "engineer in the field"?
And, if this posting makes me sound ignorant or ill-informed, please be kind in your flames...
