Finding a strong loop invariant
One loop invariant is "$n_0/n$ is a power of 2 and $n \geq 1$", where $n_0$ is the original value of $n$.

The loop invariant holds initially (before the first iteration of the loop) since $n_0 = n$, and $n_0 \geq 2$. As for what happens in the loop, there are several cases:


If $n$ is odd then $n = 2k+1$ for some $k$; since $n &gt; 1$ (otherwise the loop would have terminated), moreover $n \geq 3$, and so $n_0 = 2^t (2k+1)$ for some $t \geq 0$ and $k \geq 1$, showing that $n_0$ isn't a power of 2. 
If $n$ is even then the value of $n$ in the next iteration is $n' = n/2 \geq 1$, and so $n_0/n' = 2n_0/n$ is also a power of 2.


If the loop terminates naturally then necessarily $n = 1$, and so the loop invariant guarantees that $n_0 = n_0/n$ is a power of 2.

Finally, since $n/2 &lt; n$, the value of $n$ keeps decreasing; since always $n \geq 1$, it cannot decrease forever, i.e., the loop terminates. In fact, the running time is $\Theta(\log n)$.