[emillon]

This kind of proofs usually are separated in two steps:

- correction: define a loop invariant. Assuming the loop terminates, it will hold when the program exits the loop.

- termination: define a loop variant, something that changes at every iteration. If you can find a variant that is a strictly decreasing sequence of natural numbers (or an increasing, bounded sequence), you've established that the loop terminates.

Once you've done these two steps you know that the program terminates and the invariant holds at the end. (in your case, you won't be able to find a good variant - depending on the floating point semantics you use of course).