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.
Nagle@cup.portal.com (John - Nagle) (01/08/90)
Manual proofs are worthless (they tend to have bugs, just like programs,
and these bugs usually err in the direction of providing a
false proof) and machine proofs are very hard to do. See my paper in
ACM POPL '83. The technology progresses forward by inches, and Don
Good's group at U. Texas has done good work. Still, all successful
proof efforts that aren't bogus apply to programs of rather modest
size.
I once headed a group of five people that produced a verifier for
a dialect of Pascal. It worked, but it was too hard to use to be used
by most programmers. It's painfully difficult to convince a mechanical
theorem prover that your program is correct.
John Nagledhw@itivax.iti.org (David H. West) (01/08/90)
In article <25728@cup.portal.com> Nagle@cup.portal.com (John - Nagle) writes: > I once headed a group of five people that produced a verifier for >a dialect of Pascal. It worked, but it was too hard to use to be used >by most programmers. It's painfully difficult to convince a mechanical >theorem prover that your program is correct. I think that "most programmers" have never had access to a verifier, even a "hard to use" one. Are there any free verifiers out there? (*) -David West dhw@iti.org (*) I expect the number of available free verifiers to be so small that I don't want to discourage replies by imposing restrictions concerning language, etc. I'd be glad if the expectation were wrong.
nagle@well.UUCP (John Nagle) (01/10/90)
There are several verifiers available, none widely so. I've been
out of this field for a few years, so this isn't current information.
The Gypsy system, developed by Don Good and various others at the
University of Texas, is a code-level verifier and compiler for small
real-time programs. The verification system ran on a Symbolics when
I last saw it.
Robert Boyer and Jay Moore have a startup company in Austin called
Computational Logic, Inc., and they are working in this area.
The Pascal-F Verifier, the system I worked on, can be distributed
to academic sites. It's a code-level verifier for a real-time dialect
of Pascal. The compiler, which targeted the Intel 8061, is not available.
The verifier is written in Berkeley Pascal and Franz LISP and runs on
VAXen and Suns. It hasn't been used in years, but I could provide a copy
if someone is serious about bringing it up. See the paper, "Practical
Program Verification", in POPL '83, for more information. What it
basically undertakes to verify is that the program won't crash at
run time and that critical assertions and invariants are preserved.
Where real-time control is involved, these tend to be the crucial issues.
This system was never used for its intended purpose, verifying engine
control programs for automobiles, because the reliablity of those
programs turned out not to be a serious problem in practice.
A serious verifier is about as complicated as a serious optimizing
compiler. It's much more complicated than a simple compiler. Many
workers in the field grossly underestimated the size of the implementation
required.
Formal specifications turned out to be a dead end because they were
nearly as large as the program they specified and much harder to work on,
since you couldn't run them. But where you can specify some desired
properties, such as real-time constraints, termination, numeric values
staying within the proper limits, and such, machine proof is quite
feasible.
John Naglesnorri@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!frazierpetersja@scarlatti.CS.ColoState.Edu (james peterson) (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): >> 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; Please...is this a reference to Fetzer's article in the CACM (Sept '88) entitled "Program Verification: The Very Idea"? Or something much older? If it is Fetzer's article, Mr. Thorson's time dilation qualifies him for the relativity zone....... james lee peterson petersja@handel.cs.colostate.edu dept. of computer science colorado state university "Some ignorance is invincible." ft. collins, colorado 80523
bzs@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 mayer@rocksanne.uucp (Jim Mayer) (01/12/90)
Several messages have argued that automatic program verification is
impossible because it would require a solution to the halting problem.
While I am not a believer in automatic program verification, I do
belive that the halting problem argument does not apply here. In
particular, an automatic verifier is not required to return a result at
all... that is it can return yes/no/unknown (one can always return SOME
result by computing for a given amount of time then punting).
Some consequences of this are:
(1) If it says "YES", the program matches its specification
(but who verifies the spec?... I always felt this was the
real killer for automatic verification schemes).
(2) If it says "NO", the program does NOT match the spec.
(3) If it says "UNKNOWN", the program may or may not match
the spec. I seem to recall (no references... so reach
for your salt shaker) that some mechanism for helping
out the verifier was usually provided (even if it was
no more than an "assert" that was taken as axiomatic by
the verifier program).
-- Jim Mayer
--
Xerox Webster Research Center
Phone: (716) 422-9407 FAX: x2126 800 Phillips Road, 0128-29E
Internet: mayer.wbst128@xerox.com Webster, New York 14580dhw@itivax.iti.org (David H. West) (01/12/90)
In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart) writes: >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. I'd be more than happy to sacrifice completeness of the verifier provided that soundness is maintained (i.e. it's never wrong when it says "Verified", though it may say "Don't Know" sometimes), and provided that the verifier is at least as clever as a global optimizing compiler. -David West dhw@iti.org
yodaiken@freal.cs.umass.edu (victor yodaiken) (01/12/90)
In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart)
explains that program verification is impossible because it would violate
the halting problem theorem of Turing. This is true in a very narrow and
uninteresting sense. The problem of program verification is for programs
on actual computing devices, not programs on turing machines. If
someone produced a system which would test to see whether or not a program
could compute its intended result within the estimated life-span of the
Solar system on a computing device 100trillion times the speed of a CRAY,
the system would , by most accounts be a solution to the program
verification problem. There is nothing in unsolvability theory that
precludes such a system. Obviously, a far more modest system would
be of great practical use and theoretical interest. 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
hallett@pet16.uucp (Jeff Hallett x5163 ) (01/12/90)
In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart) writes: > >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. Proving that the output correct is an insufficient but necessary condition of overall correctness. Granted that this is somewhat of a digression, but one may overlook effects like fault masking when only examining output. > >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. This is gonna sound stupid, probably, but I'm not convinced that this is such a bad thing. Before you hit that 'F' key, let me explain a little. Turing compatibility is all well and good, but I think if we are going to have any major breakthroughs in computing technology, it will involve a step beyond Turing machines. Generally, they still are too limited to yield the results we really need. I personally feel that if we are to make any major advancements in object-oriented or AI technologies, it will involve a major change in the way we current envision programming and computing - we still think in terms of sequential steps. OO is slightly getting on the right path, but we are still forced to reduce our great data-driven systems into sequential steps. Similarly, parallel-processing is just a bunch of sequential steps happening together. I'm not claiming to be the great bearer of new and exciting breakthroughs here. I just toss out these ideas as a dreamer and speculator on the future. I don't even have an idea of what the 'new' stuff must be - but I think we are gonna need it. (howzat for specific?) -- Jeffrey A. Hallett, PET Software Engineering GE Medical Systems, W641, PO Box 414, Milwaukee, WI 53201 (414) 548-5163 : EMAIL - hallett@gemed.ge.com "Non Sequitor - Your facts are uncoordinated"; "I am Nomad: I am perfect."
henry@utzoo.uucp (Henry Spencer) (01/13/90)
In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart) writes: >>The automatic program verification proponents lost. Perlis gave a good >>talk on why... > >His arguments are significant and important practical considerations, but >there is a more fundamental theoretical issue here.... >The upshot of this is that for any language... >which is verifiable, there will be some programs that can be expressed >on a Turing Machine which cannot be expressed in this language... This is a complete red herring in the real world, however. Inability to verify arbitrary programs is irrelevant; programmers do not write arbitrary programs. It suffices to be able to verify the ones they do write. The practical problems dominate the theoretical ones here. -- 1972: Saturn V #15 flight-ready| Henry Spencer at U of Toronto Zoology 1990: birds nesting in engines | uunet!attcan!utzoo!henry henry@zoo.toronto.edu
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 <1990Jan12.164806.601@utzoo.uucp> henry@utzoo.uucp (Henry Spencer) writes: >In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart) writes: >>The upshot of this is that for any language... >>which is verifiable, there will be some programs that can be expressed >>on a Turing Machine which cannot be expressed in this language... > >This is a complete red herring in the real world, however. Inability to >verify arbitrary programs is irrelevant; programmers do not write arbitrary >programs. It suffices to be able to verify the ones they do write. The >practical problems dominate the theoretical ones here. Several people have raised this point. (I just picked a short article to follow up.) I don't dispute it, at least not absolutely. However, I do think a few considerations are in order. 1) Any language or metholodogy which has enough power to allow the expression of a Turing Machine simulator must be Turing compatible (defined by: any program that can be expressed on a Turing Machine can also be expressed in the compabible language). Now, I'm not a language designer, but I have trouble imagining a language that cannot allow the expression of a TM simulator and still be useful, since a TM simulator is a very simple program and bears some similarity to other useful programs. 2) Any verifiable language or methodology must be limited relative to a TM (as discussed in previous messages). If you give me such a language or methodology, my first reaction is to ask "What are its limits?" That's why I said one should be careful in asking for verifiability. It's a good thing when it can be achieved, but it implies limitations that need further study. Interestingly, there are a couple of good theoretical objections that I haven't seen yet. First, a computer is NOT a TM. It has finite memory. Such a system is theoretically no more powerful than a Finite Automaton. Consequently, the halting theorem doesn't really apply to computer programs. Unfortunatly, from this point of view, the verifier must be a machine much larger than the verifiee which can be a bit of a problem in practice. The second objection is that if we specify a time limit in the verification process, then the proof of the halting theorem (at least all that I've seen) falls apart. I don't know if anyone has shown whether the halting problem on programs with time limits is solvable. Also this is beginning to sound alot like the old batch systems where jobs needed a card that specified how long it was to run. Even if it needed only another second, it was unceremoniously discharged from service. Again, I'm not against verifiers (although for me, they would make programming alot less fun). However, there are serious theoretical implications, and it remains to be shown whether or not these implications carry over to the practicle domain. Brian L. Stuart Department of Computer Science Purdue University
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
baez@x.ucr.edu (john baez) (01/13/90)
In article <1862@mrsvr.UUCP> hallett@gemed.ge.com (Jeffrey A. Hallett (414) 548-5163) writes: >little. Turing compatibility is all well and good, but I think if we >are going to have any major breakthroughs in computing technology, it >will involve a step beyond Turing machines. Generally, they still are >too limited to yield the results we really need. Luckily, right now I'm perfecting my perpetual motion machine, which will generate enough energy for my time machine to send me far enough into the future to get the blueprints for a computer that computes nonrecursive functions.
arshad@lfcs.ed.ac.uk (Arshad Mahmood) (01/13/90)
In article <1990Jan12.030424.1397@world.std.com> bzs@world.std.com (Barry Shein) writes: > >The halting problem states (very roughly) "There exists at least one >program who's halting conditions cannot be determined". > >People don't often write that program*, the fact that there was one >(or a few) theoretically possible counter-example would hardly be >sufficient to invalidate the concept of automatic program >verification. No there are uncountably many of them. The undecidability of most of these problems is certainly a theoretical block, which in practice means that if you write a theorem prover to make sure that all your verifications conditions are satisfied it may loop forever. It is rarely the case that one would attack such a problem in such a naive way and usually relies on heuristics (examples include the very successfull Boyer-Moore heuristics for proving theorems about inductive LISP programs), which set of heuristics is most suitable is still undecided (surprise, surprise!) however in recent years people have developed tools for specifying and reasoning about them an example of which is Alan Bundy's "Proof Plans", however the area is still it's infancy. In practice one would not use theorem provers, and would rely instead on proof checkers. The latter rely on the user to supply the proof, but can construct skeleton proofs, maintain libraries, provide tactics and generally try and make the job simpler. This goes well with our intuition that proofs provide confidence in our programs rather than any last say about their absolute correctness (even if one had a measure for it), proofs can highlight hidden assumptions, contradictory statements in specifications, etc. I did not wish to get involved with this discussion since I found those people who objected to it not even very aware of what was happening in the field, and to say that it is largely dead is inaccurate, examples of groups working here in Britain alone are Don Sannella, Mike Fourman, Rod Burstall et al here in LFCS, Bernard Sufrin, Mike Spivey, Joseph Goguen et al in Oxford, PRG, Mike Gordon et al in Cambridge, John Darlington, Robert Kowalski et al Imperial College, there are also people in Manchester,Glasgow,London, etc. The tools developed so far are naturally somewhat basic, but 'Z' has been and continues to be used in industry. A. Mahmood Laboraory for the Foundations of Computer Science Edinburgh University Scotland
arshad@lfcs.ed.ac.uk (Arshad Mahmood) (01/13/90)
I rather invisibly moved in my last message from the halting problem to the undecidability theorem of Goedl, only the first line of my message should be linked to the halting problem the rest should be taken with regard to Goedl's famous theorem which I see as a much bigger problem than the Halting Problem. Ash
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
markh@csd4.csd.uwm.edu (Mark William Hopkins) (01/14/90)
In article <1990Jan12.030424.1397@world.std.com> bzs@world.std.com (Barry Shein) writes: > >The halting problem states (very roughly) "There exists at least one >program who's halting conditions cannot be determined". > >People don't often write that program*, the fact that there was one >(or a few) theoretically possible counter-example would hardly be >sufficient to invalidate the concept of automatic program >verification. In article <1596@castle.ed.ac.uk> arshad@lfcs.ed.ac.uk (Arshad Mahmood) writes: >No there are uncountably many of them. The fact that you are constantly writing programs that are easy to verify and understand (wherever possible) dictates that you never encounter any of the pathological cases. Therefore undecidability is actually an AID in guiding the design of your program. It's good software engineering to write your programs in a straightforward fashion as possible. So a verifier (if automated) would actively refuse to consider software beyond a certain level of complexity and "tell" you to rewrite it so that it makes sense. This not only means that verifiability is a proven concept, but that it is also a crucial tool to good software design. So, as an empirical fact, there is no humanly achievable process that cannot be emulated by verifiable software (where verification is done via a uniform algorithm).
jgk@osc.COM (Joe Keane) (01/15/90)
In article <1862@mrsvr.UUCP> hallett@gemed.ge.com (Jeffrey A. Hallett (414) 548-5163) writes: >Similarly, parallel-processing is just a bunch of sequential steps happening >together. You want something that can't be simulated on a Turing machine. You're right that adding parallelism doesn't change anything, although i don't know what would. Suppose you have a massively parallel optical computer that can compute very complex functions in very small space, and can do computations at different frequencies in the same space, and is also very big to boot. Even this could be simulated by a Turing machine, it's true. But i don't think it's a useful way to think about it. It hides a lot of the important properties of the computer. So, what is a good way to think about it? Hard to say, since i've never used such a thing.
schultz@cell.mot.COM (Rob Schultz) (01/15/90)
bzs@world.std.com (Barry Shein) writes: ...deleted... >The halting problem states (very roughly) "There exists at least one >program who's halting conditions cannot be determined". >People don't often write that program*, the fact that there was one >(or a few) theoretically possible counter-example would hardly be >sufficient to invalidate the concept of automatic program >verification. What about real-time/embedded software? If that type of software were to halt, an error must have ocurred! In general, embedded software is written as an infinite loop, with no way to exit (except to reset the processor). Does this mean that even if we can verify "normal" software, we cannot verify embedded software? ...deleted... >-- > -Barry Shein -- Thanks - Rob Schultz, Motorola General Systems Group rms 1501 W Shure Dr, Arlington Heights, IL 60004 708 / 632 - 2757 schultz@mot.cell.COM !uunet!motcid!schultz "There is no innocence - only pain." (Usual disclaimers)
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.
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.
joshua@athertn.Atherton.COM (Flame Bait) (01/17/90)
markh@csd4.csd.uwm.edu (Mark William Hopkins) writes: >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. This is called "looking for bugs" it has nothing to do with proving anything correct. I think it was Nagel who said that proofs done by hand tend to have just as many bugs as the programs they describe, and the bugs tend to falsely imply that the program works, or very similar words. >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. This might be true in general, but not me. My profs tried hard to convince me that programs are just mathamatical constructs, and could be proven just like geometry. A lot of people who teach about software, but do not write it commercially seem to think this. I think that programs are much more like biological organisms than mathmatical constructs. For example, mathmatical constructs are static over time, but organisms and programs change over time. Mathmatical constructs can not learn, but animals can learn, and programs tend to "learn" their test suites. (That last bit is a quote from a friend of mine, which has proven very true. It is not exactly like animal learning, but it is similar.) >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). I agree that such a proof would be better than nothing. But I have never seen such a proof for any real world program. One of the important parts of my argument is that the document which you so easily assumed (just like the economist of my previous posting) can not exist. Show me a machine readable specification for the compiler, linker, loader, or assember which is useful in program verification for any major operating system. Why do you think such a document is possible? Joshua Levy (joshua@atherton.com)
blenko-tom@CS.YALE.EDU (Tom Blenko) (01/17/90)
In article <1928@uwm.edu> markh@csd4.csd.uwm.edu (Mark William Hopkins) writes: |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. I am among the skeptical regarding Hopkins' claims. If he has what he says, this represents a dramatic improvement in the state of software engineering. And someone who has access to the technology can put Microsoft, for example, out of business rather quickly. I would like answers to two questions, at least one of which Hopkins didn't reply to previously: What do you do about memory aliasing? This is, according to any treatment I have encountered, a problem whose complexity increases at least exponentially with the size of the program, and for a C program it would almost certainly require global analysis of the program. How do you ensure that the specification is any good? I have worked with specifications in industry, and I'm sure I've never seen one that was complete. I probably have never seen one that is both non-trivial and consistent. So where do you get good (consistent and reasonably complete) specifications? Tom
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
UH2@PSUVM.BITNET (Lee Sailer) (01/17/90)
A tangential point. This thread started with a claim that verification is
dead. I'd hate to see the debate about a live topic, then 8-)
leeian@oravax.UUCP (Ian Sutherland) (01/18/90)
In article <11810@cs.yale.edu> blenko-tom@CS.YALE.EDU (Tom Blenko) writes: > How do you ensure that the specification is any good? This is a question which is very germane to formal verification. I've seen a lot of formal specifications that didn't say what their author meant them to say because he wasn't sufficiently careful with his use of first order logic. There are several potential ways of addressing the problem of correct formal specifications. The most obvious way is to get people to write the specifications who know how to read and write first order logic (or whatever kind of formal language you're using). Another way would be to come up with declarative languages with a formal semantics which are more perspicuous than first order logic. Yet another way is to come up with generic specifications of particular system properties that you want to verify about many systems. The particular example of this last that I've done a lot of work on is the property of being secure, in the sense that information of a particular classification cannot be inferred by an entity whose classification is not greater than or equal to that of the information. > I have > worked with specifications in industry, and I'm sure I've never > seen one that was complete. I probably have never seen one that > is both non-trivial and consistent. So where do you get good > (consistent and reasonably complete) specifications? Would you say what you mean by "consistent" and "complete"? These are very overloaded words. -- Ian Sutherland ian%oravax.uucp@cu-arpa.cs.cornell.edu Sans Peur
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!barmarmarkh@csd4.csd.uwm.edu (Mark William Hopkins) (01/19/90)
>markh@csd4.csd.uwm.edu (Mark William Hopkins) writes: >... Some software you can tell will work simply by looking at it -- >that easy they are to prove correct. In article <16692@joshua.athertn.Atherton.COM> joshua@Atherton.COM (Flame Bait) writes: >This is called "looking for bugs" it has nothing to do with proving anything >correct... No, because "looking for bugs" does not involve mathematical proof. This did. It involved proving the program correct, and thus showing that the apparent bug had nothing to do with the program (and therefore with the compiler). In this case, the proof was easy enough that it was not necessary to even write anything down: you could tell just by looking. >"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). >I agree that such a proof would be better than nothing. But I have never >seen such a proof for any real world program... ... >Why do you think such a document is possible? Because it will already exist as soon as I finish documentation on a certain "real-world" program. Assembly to boot. The only modifications to the above are the lack of compiler and operating system ... bugs are solely attributable to hardware and circuitry. This circumstance has actually materialised on a few occasions too. So, it exists. The question was never one of existence, but of responsible design.
markh@csd4.csd.uwm.edu (Mark William Hopkins) (01/19/90)
On program provability: >I am among the skeptical regarding Hopkins' claims. If he has what he >says, this represents a dramatic improvement in the state of software >engineering... Forgive me for saying so, but throughout this whole debate, I've expressed extreme skepticism of THIS claim. Surely software engineering is still not living in the dark ages! Are you implying that what I've made reference above to something completely novel?
joshua@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 utility@quiche.cs.mcgill.ca (Ronald BODKIN) (01/19/90)
In article <8421@dime.cs.umass.edu> yodaiken@freal.cs.umass.edu (victor yodaiken) writes: >... If >someone produced a system which would test to see whether or not a program >could compute its intended result within the estimated life-span of the >Solar system on a computing device 100trillion times the speed of a CRAY, >the system would , by most accounts be a solution to the program >verification problem. There is nothing in unsolvability theory that >precludes such a system. Unfortunately, untractability theory, ensures us that such a program will take up to the estimated life-span of the solar system on a computing device 100 trillion times the speed of a CRAY to solve some problems, otherwise some problems would be solvable faster than they can be solved (i.e. you can often show that a computation uses a certain amount of space, so it will halt within a given amount of time, if at all, so for it to halt within that length of time is the same as halting -- and if you could consistently, say, solve NP-hard problems in polynomial time using this machine, you'd have the result that NP-hard problems are in fact polynomial etc. etc.) So, essentially, the "halting problem" is not nearly so isolated a result. Indeed, there is NO non-trivial property of programs that can be solved, and practically it is often totally untractable to try and do these things using "finite" tricks, just like the fact that EVERY program can be written using DFA's for as large a set of input as you like, but its just foolish to try. It is, of course, still a fascinating question as to how undecidable "interesting" problems are, and to what extent things which can not be done in general can be done in special cases. Ron
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