Xref: utzoo comp.lang.c:11544 comp.arch:5765
Path: utzoo!utgpu!attcan!uunet!yale!lisper-bjorn
From: lisper-bjorn@CS.YALE.EDU (Bjorn Lisper)
Newsgroups: comp.lang.c,comp.arch
Subject: Re: compiler detection of potential run-time errors
Message-ID: <34421@yale-celray.yale.UUCP>
Date: 28 Jul 88 19:38:01 GMT
References: <1988Jul23.221743.22169@utzoo.uucp> <477@m3.mfci.UUCP> <1075@garth.UUCP> <1988Jul27.202049.21589@utzoo.uucp>
Sender: root@yale.UUCP
Reply-To: lisper-bjorn@CS.YALE.EDU (Bjorn Lisper)
Organization: Yale University Computer Science Dept, New Haven CT  06520-2158
Lines: 22

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