[racket] Checking infinite loops

On Oct 4, 2010, at 11:56 AM, Patrick Li wrote:

> Thanks for explaining that to me. I never actually looked up the formal definition of Turning-Completeness before.
> 
> So this seems rather positive. Through some clever search algorithms, or heuristics, we can have a infinite-loop checker that works well enough in practice.

That's not clear.  There are obvious source-code heuristics, such as looking for "while" loops that depend only on  unshared variables that aren't modified in the body of the loop, and there's the sure-fire approach of enumerating states of the machine and looking for duplicates... but the former misses a lot of realistic infinite-loop situations, and the latter requires that your analyzer have exponentially more memory than the program being analyzed has -- not to mention the run-time cost.  I don't know how much progress has been made on loop-checkers that "work well enough in practice."


Stephen Bloch
sbloch at adelphi.edu