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.mmm@cup.portal.com (Mark Robert Thorson) (01/08/90)
There was an excellent article about 10 years ago in CACM on this. I believe the title was "The Social Process and Proofs of Program Correctness". This article marked the death of program verification; feelings which had echoed in the halls of academia and industry for more than a decade were expressed in a clear form in print, and from that point on the "conventional wisdom" was that program verification was a dead-end for research. In retrospect, it's hard hard to see why this wasn't obvious from the very beginning.
snorri@rhi.hi.is (Snorri Agnarsson) (01/10/90)
From article <25711@cup.portal.com>, by mmm@cup.portal.com (Mark Robert Thorson): > There was an excellent article about 10 years ago in CACM on this. > I believe the title was "The Social Process and Proofs of Program > Correctness". This article marked the death of program verification; > feelings which had echoed in the halls of academia and industry > for more than a decade were expressed in a clear form in print, > and from that point on the "conventional wisdom" was that program > verification was a dead-end for research. In retrospect, it's hard > hard to see why this wasn't obvious from the very beginning. I have not read this article and I must confess it is not obvious at all to me that verification is dead. Perhaps automatic program verification is dead, that would not surprise me, but I still believe all programmers should prove their programs while they write them, even if the proofs are only for their own consumption. I believe this is especially important for large projects with many procedures. To be able to maintain a large program you need to know the following for each procedure: 1) Under what circumstances is it allowed to call the procedure? (those are the procedures preconditions) 2) Assuming it is allowed to call the procedure, what will it's effect be? (postconditions) It is astonishing how often large projects are done without documenting the above information. -- Snorri Agnarsson | Internet: snorri@rhi.hi.is Taeknigardur, Dunhaga 5 | UUCP: ..!mcvax!hafro!rhi!snorri IS-107 Reykjavik, ICELAND
frazier@oahu.cs.ucla.edu (Greg Frazier) (01/11/90)
In article <1449@krafla.rhi.hi.is> snorri@rhi.hi.is (Snorri Agnarsson) writes:
+From article <25711@cup.portal.com>, by mmm@cup.portal.com (Mark Robert Thorson):
[delete]
+> verification was a dead-end for research. In retrospect, it's hard
+> hard to see why this wasn't obvious from the very beginning.
+
+I have not read this article and I must confess it is not obvious
+at all to me that verification is dead. Perhaps automatic program
[delete]
+To be able to maintain a large program you need to know the following
+for each procedure:
+
+ 1) Under what circumstances is it allowed to call the
+ procedure? (those are the procedures preconditions)
+
+ 2) Assuming it is allowed to call the procedure, what
+ will it's effect be? (postconditions)
Different versions of verification going on here. THe
first poster meant proof when he said verification. The second
poster confidence in correctness when he said verify. Being
confident a program will work is a far cry from proving that
it will work.
Greg Frazier
...................................................................
"They thought to use and shame me but I win out by nature, because a true
freak cannot be made. A true freak must be born." - Geek Love
Greg Frazier frazier@CS.UCLA.EDU !{ucbvax,rutgers}!ucla-cs!frazierbzs@world.std.com (Barry Shein) (01/11/90)
Yes, the flap in the early 80's was over automatic program
verification. It seemed that DOD was considering putting $150M into
this so the debate became quite bloody.
The automatic program verification proponents lost. Perlis gave a good
talk on why, it went something like:
In order to determine if a program is correct another
program would have to build some sort of model to
compare it against. This would be, presumably, from
some sort of abstract specification of what the program
is supposed to do.
If the verifier could build that model it could translate
the specifications into the program. So why bother to
write a program to be verified at all? Why not just write
a high-level specifications compiler (why indeed, no one
knows how, but verification was being passed off as something
palpable to work on, like just a big math proof generator.)
There were some corrollary observations, like what exactly would such
a verifier be able to tell us? Presumably either "yes this program is
correct" or "no, this program is not correct". That's of questionable
value. If it could tell us useful detail about why it was correct or
not then, again, we are led to the conclusion that it could write the
program.
Also some amusing concerns about verifying the verifier.
--
-Barry Shein
Software Tool & Die, Purveyors to the Trade | bzs@world.std.com
1330 Beacon St, Brookline, MA 02146, (617) 739-0202 | {xylogics,uunet}world!bzsbls@cs.purdue.EDU (Brian L. Stuart) (01/12/90)
In article <1990Jan11.015531.20996@world.std.com> bzs@world.std.com (Barry Shein) writes: > >The automatic program verification proponents lost. Perlis gave a good >talk on why, it went something like: > His arguments are significant and important practical considerations, but there is a more fundamental theoretical issue here. 1) No program can be verfied to be correct unless it is verified that it produces the correct output. 2) In verifying the correctness of the output, one verifies the existence of the output. 3) Assume that a program exists that can verify the existence of output. Now create a pre-processor that takes as input a program and produces as output the same program except that it halts after every output. (The construction of such a program is left as a excercize for the reader :-) Now the combination of this pre-processor with the assumed verifier is a program which will detect whether or not a program halts. Hopefully, everyone recognizes that this is impossible according to the halting theorem, so our assumption of a program that can verify the existence of output must be false and by 1) and 2) we cannot have a program that verifies the correctness of programs in general. The upshot of this is that for any language or programming methodology which is verifiable, there will be some programs that can be expressed on a Turing Machine which cannot be expressed in this language or methodology. When you ask for verifibility, you ask to sacrifice Turing-compatability. Be careful what you ask for, you may get it. Brian L. Stuart Department of Computer Science Purdue University
joshua@athertn.Atherton.COM (Flame Bait) (01/12/90)
"Proving your programs are correct" seems to mean different things
to different people:
One group thinks it means that your program does exactly what your
spec says it should.
Another group thinks it means that you can put complex assertions
in your code and have the checker makes sure that these assertions
are always true.
The first sort of proof is obviously useless, the spec becomes the
program, and bugs in the spec become bugs in the program. Also,
specifing most programs is impossible; and if you could, then you
could write a compiler for the specification language.
The second sort of group is more interesting. It has these advantages:
It is possible.
It is not all or nothing (simple assertions can added now, and
complex ones added later on).
And these disadvantages:
Doing it well requires specific skills, which need to be taught.
It will never prove correctness; it only proves that some assertions
are true.
There are still problems getting test input data.
Joshua Levy joshua@atherton.com home:(415)968-3718
{decwrl|sun|hpda}!athertn!joshua work:(408)734-9822 snorri@rhi.hi.is (Snorri Agnarsson) (01/12/90)
From article <30689@shemp.CS.UCLA.EDU>, by frazier@oahu.cs.ucla.edu (Greg Frazier): > In article <1449@krafla.rhi.hi.is> snorri@rhi.hi.is (Snorri Agnarsson) writes: > +From article <25711@cup.portal.com>, by mmm@cup.portal.com (Mark Robert Thorson): > [delete] > +> verification was a dead-end for research. In retrospect, it's hard > +> hard to see why this wasn't obvious from the very beginning. > +... > +To be able to maintain a large program you need to know the following > +for each procedure: > + > + 1) Under what circumstances is it allowed to call the > + procedure? (those are the procedures preconditions) > + > + 2) Assuming it is allowed to call the procedure, what > + will it's effect be? (postconditions) > > Different versions of verification going on here. THe > first poster meant proof when he said verification. The second > poster confidence in correctness when he said verify. Being > confident a program will work is a far cry from proving that > it will work. No, I meant PROOF. Not automatic proof, just the usual garden variety kind of proof. Of course proofs can be wrong, so all they can do is increase our confidence. While I don't believe automatic verification is ever going to be directly useful I do believe research on those lines is useful because it increases our understanding on how to program. You can use a lot of the same techniques manually, and it is not necessary to do them formally to increase your confidence in your programs. I think every programmer should know about loop invariants, pre- and postconditions, and their use. Every programmer should know the difference between weak and strong correctness, and should know how to prove weak correctness and termination independently. Every programmer should know how to prove weak correctness of mutually recursive procedures, and why the method works. Every programmer should be able to state and prove data invariants for their data types. I find it very hard to understand why some people claim we should not use these techniques just because they do not give us 100% confidence in our programs. Similar reasoning should tell us to abandon testing, and should tell mathematicians to stop writing theorems. -- Snorri Agnarsson | Internet: snorri@rhi.hi.is Taeknigardur, Dunhaga 5 | UUCP: ..!mcvax!hafro!rhi!snorri IS-107 Reykjavik, ICELAND
desnoyer@apple.com (Peter Desnoyers) (01/13/90)
In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.EDU (Brian L. Stuart) writes: >[flawed proof that program verification is impossible.] Try this one instead. Given a program V that will verify whether or not program P run on input I will produce output O. We can transform P by deleting all output statements and having it output a single value O' before it halts. [ie. transform P() to P'(),print(O') where P'() is P() with all print statements deleted.] V(P',I,O') will then determine whether or not the output of P'(I) is O', which is equivalent to determining whether P(I) halts. Therefore V cannot exist. However, this result isn't as useful as it seems. First, there are important classes of programs where V is computable, even if it is not computable on all programs. Second, program verification often means proving whether or not P (the program) is equivalent to P' (the specification), which is a different problem entirely. (although probably not computable in the general case.) Peter Desnoyers Apple ATG (408) 974-4469
bls@cs.purdue.EDU (Brian L. Stuart) (01/13/90)
In article <6158@internal.Apple.COM> desnoyer@apple.com (Peter Desnoyers) writes: >In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.EDU (Brian L. Stuart) >writes: >>[flawed proof that program verification is impossible.] > >Try this one instead. Given a program V that will verify whether or not >program P run on input I will produce output O. We can transform P by >deleting all output statements and having it output a single value O' >before it halts. [ie. transform P() to P'(),print(O') where P'() is P() >with all print statements deleted.] V(P',I,O') will then determine whether >or not the output of P'(I) is O', which is equivalent to determining >whether P(I) halts. > >Therefore V cannot exist. This appears to me to also be a valid proof from the case of verifiers with the specified form. >However, this result isn't as useful as it >seems. First, there are important classes of programs where V is >computable, even if it is not computable on all programs. Second, program >verification often means proving whether or not P (the program) is >equivalent to P' (the specification), which is a different problem >entirely. (although probably not computable in the general case.) Not entirely. Anytime a program is verified, the correctness of its output is verified either implicitly or explicitly. That is why I was careful to phrase my proof in a form that did not say that verification took place by verifying output, but instead took the general case of a verifier. I said that a by-product of the verification process was the verification of output and used that. Why do you feel that my proof was flawed? I know its not as rigorous as it could be, but I don't thing its wrong. Brian L. Stuart Department of Computer Science Purdue University
desnoyer@apple.com (Peter Desnoyers) (01/13/90)
In article <9237@medusa.cs.purdue.edu> bls@cs.purdue.EDU (Brian L. Stuart) writes: > Why do you feel that my proof was flawed? I know its not as rigorous > as it could be, but I don't thing its wrong. Your proof was of the form "take program P and transform it into program P'. Verifying that P produces any output is the equivalent of solving the Halting Problem for P'". In other words, you showed that you could use a program that decides the Halting Problem to decide the verification problem. That isn't a particularly interesting result (since halting problem deciders can compute just about anything :-) - what we need to prove that the verifier cannot exist is to show that you can use the verifier to solve the halting problem. Don't feel bad - I think I made the identical mistake on the net a year or two ago. Peter Desnoyers Apple ATG (408) 974-4469
snorri@rhi.hi.is (Snorri Agnarsson) (01/14/90)
From article <16479@joshua.athertn.Atherton.COM>, by joshua@athertn.Atherton.COM (Flame Bait): > "Proving your programs are correct" seems to mean different things > to different people: > > One group thinks it means that your program does exactly what your > spec says it should. > > Another group thinks it means that you can put complex assertions > in your code and have the checker makes sure that these assertions > are always true. And a third group (including myself) thinks it means you can put assertions in your code and in your interfaces and carefully try to see to it that those assertions are true at each time point. This is not very hard at all for good programmers (in fact I would claim that those who cannot do this cannot be good programmers), and has the extra advantage that the assertions act as documentation for future maintenance. -- Snorri Agnarsson | Internet: snorri@rhi.hi.is Taeknigardur, Dunhaga 5 | UUCP: ..!mcvax!hafro!rhi!snorri IS-107 Reykjavik, ICELAND
joshua@athertn.Atherton.COM (Flame Bait) (01/16/90)
kers@hplb.hpl.hp.com (Kers) writes: >I'll also think that the remark "specifying most programs is impossible" is >wrong. "bloody difficult, especially after the fact" is the predicate that >springs to mind. No problem. Specifiy the following programs, in a machine readable format useful to a program verifier. These should be commerical products, so they must look good and feel good so that people want to use them: A rule based expert system shell. Remember to specify input and output for an window based system. A source code control facility like SCCS or RCS If you use system calls you must have some way of proving that they do what your spec says they do. <Put most any real world program here> My last example points out a current problem with proving program correct. They must only use libraries which have been proven correct, must run on an operating system which has been proven correct, and must use hardware which is proven correct. All of this is impossible right now. I'm serious about this challenge. I hold that these program can not be specified in any kind of useful way, and that the set of programs which can be proven correct is so small as to be uninteresting. I assume everyone has heard the joke about three people (a chemist, a physist, and an economist) who are trapped on a desert island with only cans of food. The punch line is the economist saying "Imagine a can opener". I often think of this branch of the "software proof" camp in the same way. As long as they stick to mathmatical programs which do not have input, output, or any other real life constraints, they can create interesting examples. Joshua Levy joshua@atherton.com home:(415)968-3718 {decwrl|sun|hpda}!athertn!joshua work:(408)734-9822
joshua@athertn.Atherton.COM (Flame Bait) (01/16/90)
In article <1455@krafla.rhi.hi.is> snorri@rhi.hi.is (Snorri Agnarsson) writes: >From article <16479@joshua.athertn.Atherton.COM>, by joshua@athertn.Atherton.COM (Flame Bait): >> Another group thinks it means that you can put complex assertions >> in your code and have the checker makes sure that these assertions >> are always true. > >And a third group (including myself) thinks it means you can put >assertions in your code and in your interfaces and carefully >try to see to it that those assertions are true at each time point. I would group you into my second group. The assertions are checked both statically and dynamically. By the way, I agree that this is good programming practice and I do it myself, but it is not "proving a program correct". I consider it part of defence in depth. Joshua Levy joshua@atherton.com home:(415)968-3718 {decwrl|sun|hpda}!athertn!joshua work:(408)734-9822
markh@csd4.csd.uwm.edu (Mark William Hopkins) (01/16/90)
In article <16664@joshua.athertn.Atherton.COM> joshua@Atherton.COM (Flame Bait) writes: >My last example points out a current problem with proving program correct. >They must only use libraries which have been proven correct, must run on >an operating system which has been proven correct, and must use hardware >which is proven correct. All of this is impossible right now. A program verification would look like this: "This program is guaranteed to operate consistently with the specifications outlined in the adjoining document on a CORRECT compiler and operating system. Any apparent bugs found are solely attributable to one or more of the utilities used to form the environment of the program." (the document could be short for all we care, just so long as it specifies all the details relevant to the user). Just because a program may be operating in a faulty environment does not mean that verification cannot be done with it. Verification is ALWAYS done conditionally on the assumption that everything being used to support the software is correct. In this context, it's only purpose is to eliminate the sources of possible bugs (it can't be the software, so it must be the firmware or even the hardware(!)). And by verification I DO mean mathematical verification. Of course, you will do some actual run-time testing whose purpose is to aid in the discovery of the mathematical properties of the software. That way you can significantly automate much of the discovery process. That's how I've been able to detect bugs in system utilities, such as a local Pascal compiler, an assembler, and even circuitry quite a few times. Never managed to find fault with a chip yet though... It's funny, because a student once came to me with a 200-300 line Pascal program, trying to figure out what was wrong with it. I looked at it in detail, and simply by inspection could tell her that there was nothing wrong with it. Some software you can tell will work simply by looking at it -- that easy they are to prove correct. So ... it was the compiler. The mentality was so ingrained in people (which was actually picked up from the course) that programs are creatures to be analysed behaviorally, instead of mathematical constructs, that it simply never occurred to this person that she might be able to prove that the fault did not lie with her program. >I often think of this branch of the "software proof" camp in the same way. >As long as they stick to mathmatical programs which do not have input, >output, or any other real life constraints, they can create interesting >examples. The irony...
jimad@microsoft.UUCP (JAMES ADCOCK) (01/17/90)
Given that real-world commercial software products of typical size have thousands, if not tens-of-thousands of bugs discovered before shipping, and that most of those bugs have to be fixed, and a few passed over, it seems that one would be better off *not* trying to prove that your [non-trivial] piece of code is correct, but rather understanding when a piece of code fails, under what conditions, and make sure you have the most important day-to-day situations covered. The way one discovers bugs in one's software is not by trying to prove its correct, but rather by trying to show it is incorrect, and how. Trying to 'prove' software is correct does nothing to improve the quality of the software involved. Finding and removing bugs does. The trick is to try to find and fix as many bugs as cheaply as possible in a reasonable amount of time. Is a new, high quality car free of bugs? NO -- it has hundreds or thousands of engineering and manufacturing imperfections. Likewise any reasonably sized piece of software. Rather than try to 'prove' your auto is perfect, better to test that the wheels don't all fall off while driving down the freeway at 60 miles an hour. Again: 'proving' that software is correct does nothing to improve the quality of that software. Finding and removing bugs does improve the quality of software. Find and remove the worst bugs as cheaply as possible in order to create the highest quality of software you can produce. The cheapest bug to remove is the one that was never introduced. And you can't introduce bugs in code never written. So only write code for the most needed features. And make sure you wring most of the bugs out of those features. The proper approach to quality software has more to do with Shewhart and Deming than Turing. Standard disclaimer.
duncan@dduck.ctt.bellcore.com (Scott Duncan) (01/17/90)
In article <10289@microsoft.UUCP> jimad@microsoft.UUCP (JAMES ADCOCK) writes: > Trying to >'prove' software is correct does nothing to improve the quality of the software >involved. Finding and removing bugs does. The trick is to try to find >and fix as many bugs as cheaply as possible in a reasonable amount of time. Actually, as is pointed out below, the "trick" is to avoid introducing defects in the first place or find them before code gets written. While it is true that the writing of code can introduce defects, most people's investigations in defect analysis suggest that a substantial proportion of defects result from requirements, specification, or design problems rather than coding ones. >Is a new, high quality car free of bugs? NO -- it has hundreds or thousands >of engineering and manufacturing imperfections. Likewise any reasonably >sized piece of software. I would submit that the number of parts/pieces/etc. in many manufactured items relative to the number of critical ones -- ones that can cause malfunction -- is higher than that in software. That is, it is more likely that defects in software will produce malfunction than manufacturing imperfections since soft- ware describes a process more than a product. Each step of the process des- cription is important -- otherwise it shouldn't be there (as is also pointed out below). (I would agree that many defects in manufactured products make them less de- sirable to use, but many affects appearances and looks only rather than the safety issue implied by the example below. In software, even the "looks" of software systems can impair their effective use by the customer. Hence the concern for human factors in software.) > Rather than try to 'prove' your auto is >perfect, better to test that the wheels don't all fall off while driving >down the freeway at 60 miles an hour. I believe that the primary job of testing and quality assurance is to try to "prove" a product or software system is not perfect. And, hence, to point out problems in the process -- manufacturing or development -- which created it. I am somewhat in agreement with the attitude expressed here, therfore, and the implied philosophy of identifying what is critical and making sure that/these part(s) function properly. >Again: 'proving' that software is correct does nothing to improve the >quality of that software. True, but then the thrust, as I understand it, is not to improve the quality through proof, but to verify the quality (or lack of it). > Finding and removing bugs does improve the >quality of software. This approach, however "practical," does seem to suggest some giving-in to the inevitability of defects. Perhaps a better approach, all around, would be to investigate the applicability of statistical quality control methods which, if I read the literature on Japanese development efforts correctly, attempt to determine just how much testing is needed to remove cerrtain levels of defects. > Find and remove the worst bugs as cheaply as >possible in order to create the highest quality of software you can produce. Presumably, the statistical approaches are focused on doing just that. >The cheapest bug to remove is the one that was never introduced. And you >can't introduce bugs in code never written. So only write code for the >most needed features. As noted above, I quite agree. It is unfortunate that most productivity mea- sures applied to spftware (be they lines of code, function points, etc.) seem to emphasize producing more code or more features rather than meauring how little code or how few features can be producedd to accomplish the task. >The proper approach to quality software has more to do with Shewhart >and Deming than Turing. Speaking only for myself, of course, I am... Scott P. Duncan (duncan@ctt.bellcore.com OR ...!bellcore!ctt!duncan) (Bellcore, 444 Hoes Lane RRC 1H-210, Piscataway, NJ 08854) (201-699-3910 (w) 609-737-2945 (h))
ian@oravax.UUCP (Ian Sutherland) (01/17/90)
In article <10289@microsoft.UUCP> jimad@microsoft.UUCP (JAMES ADCOCK) writes: >The way one discovers bugs in one's software is not by trying to prove its >correct, but rather by trying to show it is incorrect, and how. Trying to >'prove' software is correct does nothing to improve the quality of the software >involved. Finding and removing bugs does. I have found bugs in software by trying to prove it's correct. In the course of trying to prove it's correct, you realize at some point that it is NOT correct, and the failure of the proof actually points out the bug. Here's a simple but amusing example. Consider the following C program which is intended to swap the values in 2 integer locations: void swap(x,y) int *x; int *y; { int temp; temp = *x; *x = *y; *y = temp; } Looks correct, doesn't it? I tried to verify this program as a simple example in a C verification system we built at the company I work for. In the course of trying to verify it, I started seeing various expressions being generated of the form "if the value in x and the location of temp are the same then A else B". I thought this was a bug in the verifier until I realized that there's nothing about the above program which ensures that swap is not passed a pointer to the location where temp gets put. In fact, once you think about this, it turns out to be pretty easy to get this bug to manifest itself. In other words, the above program does not correctly swap the contents of the 2 locations it's passed in all cases. Not only did attempting to verify the program turn up this bug, but it told us exactly under what circumstances the program will malfunction. It's my experience that verification not only helps you find bugs, but helps you find the ones that you'd be least likely to find by other methods. It's not economical to use on large systems at the moment, but it's getting there, and there are plenty of programs which are not so large whose correctness is nonetheless critical to the system they're a part of. -- Ian Sutherland ian%oravax.uucp@cu-arpa.cs.cornell.edu Sans Peur
markh@csd4.csd.uwm.edu (Mark William Hopkins) (01/17/90)
In article <10289@microsoft.UUCP> jimad@microsoft.UUCP (JAMES ADCOCK) writes: >Given that real-world commercial software products of typical size have >thousands, if not tens-of-thousands of bugs discovered before shipping,... You seem so overly predisposed to the prejudice of "programming as engineering" as to unnecessarily exclude a concept that is already proven to work. For example, the program I made reference to in a previous article as already having verified, optimized, and upgraded added to 4000 lines and the analysis took 2 weeks. Because of the enormous amount of knowledge of that software gathered during the proof process, I can literally go into it and make modifications to it in under a minute (whenever the specification is upgraded). In fact a 200 line extension took an hour to write, and was proven bugfree before the first run. On another occasion, a 1000 line parser generator took one night to prove consistent with its design, and was subsequentally coded in two days without a single error (though the design itself had one minor easily corrected flaw). So... size is simply not an obstacle. It's just a matter of having the competence to carry out such an analysis. >Again: 'proving' that software is correct does nothing to improve the >quality of that software. To prove a piece of software correct means to prove that is does not have any bugs in it (i.e. there is no inconsistency between specification and implementation). It also means to optimize the software using the newly found information gathered during the proof process on its implementation, and my experience has been that most if not all software beyond a certain scale (that has not already undergone this type of analysis) can be optimized by at least 50% if not more (while simultaneously upgrading its functionality, readibility, and verifiability). In my book, showing that a piece of software has no bugs in it is a MAJOR improvement on its quality, especially when done in conjunction with the subsequent optimizations. It leads major improvements in design. In addition, when the software is encumbered by the addition of signal processing routines and interrupts, it proves to be a NECESSITY to verify mathematically its proper functioning. I would consider it irresponsible design if such software was distributed and was not verified against race conditions and things of the like.
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.
snorri@rhi.hi.is (Snorri Agnarsson) (01/17/90)
From article <16664@joshua.athertn.Atherton.COM>, by joshua@athertn.Atherton.COM (Flame Bait): > ... > My last example points out a current problem with proving program correct. > They must only use libraries which have been proven correct, must run on > an operating system which has been proven correct, and must use hardware > which is proven correct. All of this is impossible right now. This is simply a problem of programming in general and has very little to do with program proving. When you prove something you generally have to make some assumtions, in this case you would naturally assume that the descriptions you have for library and system subroutines are correct. Where is the advantage of NOT proving your program correct? > I'm serious about this challenge. I hold that these program can not > be specified in any kind of useful way, and that the set of programs > which can be proven correct is so small as to be uninteresting. In that case the set of useful, trustworthy programs you CANNOT prove correct must be large and interesting. Would you care to give us some examples? Perhaps at the same time you could prove that they are correct and trustworthy, but not provable! -- Snorri Agnarsson | Internet: snorri@rhi.hi.is Taeknigardur, Dunhaga 5 | UUCP: ..!mcvax!hafro!rhi!snorri IS-107 Reykjavik, ICELAND
snorri@rhi.hi.is (Snorri Agnarsson) (01/17/90)
From article <16665@joshua.athertn.Atherton.COM>, by joshua@athertn.Atherton.COM (Flame Bait): > In article <1455@krafla.rhi.hi.is> snorri@rhi.hi.is (Snorri Agnarsson) writes: >>And a third group (including myself) thinks it means you can put >>assertions in your code and in your interfaces and carefully >>try to see to it that those assertions are true at each time point. > I would group you into my second group. The assertions are checked > both statically and dynamically. By the way, I agree that this is > good programming practice and I do it myself, but it is not "proving > a program correct". I consider it part of defence in depth. I usually just check the assertions statically myself, unassisted, and the assertions are simply comments in the program text, not executable statements. Arguing about whether this is a proof or not will not get us far. I claim this is a proof in the usual mathematical sense. Some people seem to think a proof is not a proof until a proof checker has validated it. I disagree. Validation by a proof checker would give me more confidence in a proof, that's all. I agree that this is part of defence in depth, so perhaps we only disagree on the definition of the word "proof". -- Snorri Agnarsson | Internet: snorri@rhi.hi.is Taeknigardur, Dunhaga 5 | UUCP: ..!mcvax!hafro!rhi!snorri IS-107 Reykjavik, ICELAND
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.hawley@icot32.icot.jp (David John Hawley) (01/18/90)
In article <10289@microsoft.UUCP> you write: >... >The way one discovers bugs in one's software is not by trying to prove its >correct, but rather by trying to show it is incorrect, and how. Trying to >'prove' software is correct does nothing to improve the quality of the software >involved. Finding and removing bugs does. The trick is to try to find >and fix as many bugs as cheaply as possible in a reasonable amount of time. >Is a new, high quality car free of bugs? NO -- it has hundreds or thousands >of engineering and manufacturing imperfections. Likewise any reasonably >sized piece of software... I think this analogy is misguided. The proper analogy with manufacturing and software would be that the manufacturing process (software) has flaws and these result in unacceptably high-levels of flawed goods (output). It is important to note that there is one process and multiple instances of its output. It seems more efficient to fix the process than fix each output item. It's maybe even better to design the process the right way in the first place. Actually I agree with what has been said in this newsgroup about concentration on formal specifications obscuring the real problem which is modelling the real world, but it is also nice to know that your models are faithfully represented in your experiments (programs). Returning to the article quoted above, since the analogy is bad I can't see any merit in the conclusions.
barmar@think.com (Barry Margolin) (01/18/90)
In article <1248@oravax.UUCP] ian@oravax.odyssey.UUCP (Ian Sutherland) writes:
] void swap(x,y)
] int *x;
] int *y;
] {
] int temp;
]
] temp = *x;
] *x = *y;
] *y = temp;
] }
]In the course of trying to verify it, I started seeing various
]expressions being generated of the form "if the value in x and the
]location of temp are the same then A else B". I thought this was a bug
]in the verifier until I realized that there's nothing about the above
]program which ensures that swap is not passed a pointer to the location
]where temp gets put.
Since the expression &temp never appears, there is no valid way to have a
pointer to temp. It's possible to have a pointer which happens to have the
address of temp in it, but that would be due to invalid code elsewhere in
the program. For instance, if a pointer to an automatic variable is stored
in a global variable or returned from a function then it may later point to
an automatic variable in a different function. This is essentially the
same as using an uninitialized pointer variable.
When verifying a program, certain assumptions must be made. People have
already pointed out that you must assume that the supporting facilities
(the compiler, the runtime library, the hardware) behave as documented, you
must also assume that a function is called validly when verifying that
function in isolation. Otherwise, one could claim that the above function
doesn't operate properly when passed the wrong number of arguments, or when
passed integers (rather than pointers to integers), or when passed pointers
to non-integers. Verifying the above function amounts to saying that
adding it to a correct program will not make that program incorrect.
--
Barry Margolin, Thinking Machines Corp.
barmar@think.com
{uunet,harvard}!think!barmarjoshua@athertn.Atherton.COM (Flame Bait) (01/19/90)
This is a reply to article <1248@oravax.UUCP> ian@oravax.odyssey.UUCP,
written by Ian Sutherland. Please look at that posting to see his bogus
example.
Ian: please learn C (and teach it to your proof system) before posting
examples using it. In your example temp is an automatic (or local)
variable, while a and b are parameters passed into the function which
contains temp. There is no way in C for temp to be the same variable
as either a or b. If temp were a static or a global, there would be
a problem. Note that calling swap recursively will work fine given
your example.
This all assumes a working compiler, linker, and runtime, of course.
Joshua Levy joshua@atherton.com home:(415)968-3718
{decwrl|sun|hpda}!athertn!joshua work:(408)734-9822 jug@itd.dsto.oz (Jim Grundy) (01/20/90)
From article <16773@joshua.athertn.Atherton.COM>, by joshua@athertn.Atherton.COM (Flame Bait): > This is a reply to article <1248@oravax.UUCP> ian@oravax.odyssey.UUCP, > written by Ian Sutherland. Please look at that posting to see his bogus > example. > > Ian: please learn C (and teach it to your proof system) before posting > examples using it. In your example temp is an automatic (or local) > variable, while a and b are parameters passed into the function which > contains temp. There is no way in C for temp to be the same variable > as either a or b. If temp were a static or a global, there would be > a problem. Note that calling swap recursively will work fine given > your example. Try this (The dummy var has been added so that this procedure has the same signature as the original swap and so a call to it will take up the same stack space) void GetAnAddressOffStack(AddressOnStack, dummy) int *AddressOnStack, dummy; { int TemporaryVariableOnTheStack; AddressOnStack = &TemporaryVariableOnTheStack; } main() { int *AddressOnStack, x, dummy; GetAnAddressOffStack(AddressOnStack &dummy); x = 1; *AddressOnStack = 2; swap(&x, AddressOnStack); printf("&d, &d", x, *AddressOnStack); } Now when swap is called, it's local variable temp will have the same address as the value contained its second parameter y. The printf is going to give you "1, 1". JIM Truely falme bait is what his name suggests
windley@cheetah.ucdavis.edu (Phil Windley/20000000) (02/03/90)
I keep hoping to let this one drop, but people keep making comments that I
just can't let go by. If you're tired of reading this, push "k" now.
In article <10417@microsoft.UUCP> jimad@microsoft.UUCP (JAMES ADCOCK) writes:
I think it is a gross distortion of reality to state that a program
that in actually crashes is "correct" because it has been "proven" to
be so. A real world customer tries running your "proven" correct
spreadsheet and finds that your program crashes when other than trivial
math expressions are requested of it. So said customer calls you up
and you say: "I'm sorry sir, but that program *has* been proven correct!"
BFD.
No one who knows what verification is would ever say that anymore than
Boeing would say in response to an airplane crash "I'm sorry, our
computational fluid dynamics models don't predict that failure, so you're
airplane must still be flying."
Verification *IS NOT* about proving things about real computers and real
programs running on real computers. It is about proving things about
models of real computation. Now, if your contention is that nothing a
model can tell me is worthwhile, then you'll never see any use in
verification (or most of applied mathematics). I'm here to tell you that
models are important and that the things that verification can tell you are
important. I'm not going to claim that it will prove that a program
works.
Verification does not provide "knowledge" in the philosophical sense, it
provides "justified true belief" which is the next best thing.
--
Phil Windley | windley@cheetah.ucdavis.edu
Division of Computer Science | ucbvax!ucdavis!cheetah!windley
University of California, Davis |
Davis, CA 95616 | (916) 752-6452 (or 3168)