jdike@karaya.com (Jeff Dike) wrote on 02.01.00 in <200001030217.VAA05240@ccure.karaya.com>:
> > I'm not sure that the well-known theoretical insolubility of the
> > halting problem implies that one cannot formally and tractably
> > compute other meaningful and useful execution properties of an
> > arbitrary procedural program.
>
> It does mean that there are cases (in principle) where computing execution
> properties of a program is exquivalent to the halting problem. You can
> encode anything you want in terms of a halting problem.
>
> I haven't worried about this because:
> there aren't going to be too many halting problems in typical code
> there shouldn't be any halting problems in your code anyway
/*SLINT some_preconditions*/
while (complicated_condition()) complicated_calculation();
/*SLINT some postconditions*/
might well be something the lint cannot prove works. Say what you're doing
here is applying some complicated mathematical theorem; the lint doesn't
know about that theorem and cannot prove it, because that'd be the halting
problem.
It can, however, verify the rest of the program and tell you that all's
fine except for these lines, where it can't prove the postconditions from
the preconditions.
This should be enough in praxis. And for testing, you can often add an
assertion.
MfG Kai
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu
Please read the FAQ at http://www.tux.org/lkml/
This archive was generated by hypermail 2b29 : Fri Jan 07 2000 - 21:00:07 EST