P-NP problems solved? FindBugs solves the halting prob?

Question

There is a tool called FindBugs it can detect infinite never ending loops in a given program/ code base.

This implies FindBugs can detect if a program will end or not by analyzing the code. Halting problem is the problem defining that:

Given a description of an arbitrary computer program, decide whether the program finishes running or continues to run forever

So does this imply that the halting problem is solved or a subset of the halting problem is solved?

Answer 1

No, it's not solved. Findbugs only finds some of the cases of infinite never ending loops, such as this one:

public void myMethod() {
    int a = 0;
    while (true) {
        a++;
    }
}

IIRC, the only false negative it suffers from is, if the above method myMethod is never called, in which case you 'll still want to delete it as it's dead code.

It does suffers from false positives: there are many cases of non-ending programs that findbugs will not detect.

Answer 2

Imagine that you have a tool that always detects infinite loops.

Suppose there exists a unievrsal machine HALT(CODE, INPUT) that halts iff CODE halts on INPUT. Now consider this:

1. if HALT(CODE, CODE), loop forever
2. else halt

If CODE halts on CODE, you'll get a contradiction, and also if it doesn't. Why?

Assuming CODE halts on CODE, then the program will loop forever.. meaning that... it doesn't stop..
Now assume that CODE doesn't halt on CODE, you'll get that.... it does stop..

Answer 3

If you were to make a program to analyze a program for the same platform with the same limits as the analyzing programs it's impossible for such analyzer to exist. This is known as the halting problem.

When that said, halting problem is solvable for programs that has a lot less memory consumption and code length than the analyzing program can have. Eg. I can make a halt? procedure for all 2 byte BrainFuck-programs like this:

;; takes a valid 2 byte BF-program
;; and returns if it will halt
(define (halt? x)
  (cond ((equal? x "[]") #f)
        (else #t)))

A larger example is by making an interpreter and hash memory states and pc-location. If a previous state is found it's an infinite loop. Even with a very good data model the memory used by the interpreter must be considerable larger than what it interprets.

I'm thinking of constant folding programs by doing and the halting problem becomes an issue. My idea is to have a data structure that has the number of times a particular branch in AST has been seen and have a cutoff limit that is very large. Thus if the interpreter has been at a branch more than the cutoff it will end up in the compiled program instead of it's computation. It takes a lot less memory and will establish that some or all parts of a program certainly does return (halt).

Imagine this code:

(define (make-list n f)
   (if (zero? n)
       '()
       (cons (f) (make-list (- n 1) f))))

(define (a)
  (b))

(define (b)
  (c))

(define (c)
  (b))

(display (make-list 4 read))
(display (make-list 4 a))

It's actually pretty bad code since you don't know which order the input might get. The compiler get to choose whats best and it might turn into:

(display-const "(")
(display (read))
(display-const " ")
(display (read))
(display-const " ")
(display (read))
(display-const " ")
(display (read))
(display-const ")")
(display (cons (b) (cons (b) (cons (b) (cons (b) '())))) ; gave up on (b)