# Finding a strong loop invariant

Pseudocode:

if n < 2
return false
while n != 1
if n % 2 != 0
return false
n = n/2
return true


The loop will terminate when n is odd. If n = 1, true is returned and that means that n0 was a power of 2. Otherwise it's false.

I'm new at this and struggle with the proving the power of 2 part for before and during iterations and after the loop terminates. Also what does a loop invariant look like for a true vs false return on a loop?

Is it reasonable to say something like:

at the every iteration i, 1 <= n <= n0/(2^i)
true returned when n = 1 and n0 is a power of 2
false returned when n is odd and n > 1

Is it possible to even make strong loop invariant here without referencing the initial value of n?

• The loop invariant is that $n_0/n$ is a power of 2, where $n_0$ is the original value of $n$. The loop terminates since $n$ always decreases. – Yuval Filmus Sep 27 '18 at 2:41
• Thanks for responding to me. How were you able to find that pattern? Is it just from experience and practice? – weztex Sep 27 '18 at 4:18
• I'm not sure what's the difference between experience and practice. In college and beyond, you should never solve 100 exercises of the form "3+4=?". A few should suffice. Your problem-solving skills improve with time, and experience with one thing could help with another. – Yuval Filmus Sep 27 '18 at 4:20

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 > 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 < 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)$$.