henry@utzoo.uucp (Henry Spencer) (07/28/88)
In article <1075@garth.UUCP> smryan@garth.UUCP (Steven Ryan) writes: >Depends on whether all possible programs (including those of monkey >programmers) or just `practical' programs are considerred. Formal proofs >of all possible programs are impossible, flat out, no appeal. Formal proofs >of practical programs depend on how powerful practical has to be to remain >useful. My standing comment on this one is "programmers do not write arbitrary programs". I have no objection to monkey programmers being told "this program is so poorly written that verifying the absence of run-time errors is beyond this compiler's ability". In fact, I have no objection to real programmers occasionally getting the same message, provided some attempt is made to identify the source of the problem. As it is, I occasionally have to modify my programs to keep less-than-perfect implementations of cc or lint happy; an absence-of-run-time-errors checker that required "unnecessary" changes once in a while would still be worth having. (I also wonder whether proving absence of run-time errors is sufficiently weaker than proving correctness that it is fundamentally easier, but on reflection it seems to me that in the [irrelevant] general case it is probably equivalent to the halting problem.) -- MSDOS is not dead, it just | Henry Spencer at U of Toronto Zoology smells that way. | uunet!mnetor!utzoo!henry henry@zoo.toronto.edu
lisper-bjorn@CS.YALE.EDU (Bjorn Lisper) (07/29/88)
In article <1988Jul27.202049.21589@utzoo.uucp> henry@utzoo.uucp (Henry Spencer) writes: .... >(I also wonder whether proving absence of run-time errors is sufficiently >weaker than proving correctness that it is fundamentally easier, but >on reflection it seems to me that in the [irrelevant] general case it is >probably equivalent to the halting problem.) To find whether a program is free from run-time errors or not is of course undecidable in general. One type of run-time errors is array indices getting out of bounds. Say, for instance, that we have an ARRAY a(1..n) and somewhere in the program a statement a(i) := .... . In order to prove absence of sun-time errors in this program we must prove that always 1 <= i <= n immediately before this statement. Since we can do arbitrary integer operations on i before this point this amounts to deciding the truth of an arbitrary formula in integer arithmetic. Thus it is undecidable. Of course there are many *special* cases where freedom from run-time errors can be decided. So I'm not saying that compile-time checking of such properties is futile. On the contrary, I think it can be very useful. Bjorn Lisper
smryan@garth.UUCP (Steven Ryan) (07/30/88)
>My standing comment on this one is "programmers do not write arbitrary >programs". I have no objection to monkey programmers being told "this >program is so poorly written that verifying the absence of run-time errors >is beyond this compiler's ability". In fact, I have no objection to real >programmers occasionally getting the same message, provided some attempt >is made to identify the source of the problem. A point to remember is the compiler doesn't know who or what wrote the code. I take it then the idea to do prove what can be proved, refute what can be refuted, and it's the middle ground which is rejected. I see no objections to this approach if it is well defined.