Hey, as a once (medium long ago) CS major myself, I'd like to comment on your question. I think you're not really referring to Godel's Incompleteness Theorem, which relates more to axiomatic systems then it does to computer programs / algorithms, but to Turing's proof that
the halting problem is algorithmically undecidable. The halting problem here is the problem of deciding whether a certain algorithm will run forever or ever halt. Algorithmically undecidable here means that it is impossible for you to build an algorithm such that for any given input program P, your algorithm will say whether or not the program P will ever halt. Important remark: this does not mean that it is impossible for you to prove that a specific program P1 halts or doesn't halt. It just means that it is impossible to write down an algorithm for doing it in all cases. It is even impossible to decide for which cases it is possible and for which not.
A consequence (or more generalized version if you will) of the fact that the halting problem is algorithmically undecidable is that the static analysis problem is also algorithmically undecidable. Static analysis here is the task of deciding whether a program P satisifies a specification S. You can not write an algorithm such that for any combination (S,P) the algorithm will tell you whether the program satisfies the spec or not. That again does not mean that it is impossible to prove that an individual program P1 satisfies an individual specification S1, which appears to be the case here.
To quote wikipedia on the halting problem:
http://en.wikipedia.org/wiki/Halting_problem
While Turing's proof shows that there can be no general method or algorithm to determine whether algorithms halt, individual instances of that problem may very well be susceptible to attack. Given a specific algorithm, one can often show that it must halt for any input, and in fact computer scientists often do just that as part of a correctness proof. But each proof has to be developed specifically for the algorithm at hand; there is no mechanical, general way to determine whether algorithms on a Turing machine halt. However, there are some heuristics that can be used in an automated fashion to attempt to construct a proof, which succeed frequently on typical programs. This field of research is known as automated termination analysis.
