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?