[comp.lang.c] compiler detection of potential run-time errors

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.