This kind of proofs usually are separated in two steps:<p>- correction: define a loop invariant. <i>Assuming the loop terminates</i>, it will hold when the program exits the loop.<p>- termination: define a loop <i>variant</i>, 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&#x27;ve established that the loop terminates.<p>Once you&#x27;ve done these two steps you know that the program terminates and the invariant holds at the end. (in your case, you won&#x27;t be able to find a good variant - depending on the floating point semantics you use of course).