Understanding Log(n) Loop Invariant

Question

When attempting to find the following loop invariant for:

int log(int x)
{ 
  int i = 0;
  int j = x;
  while (j > 1) {
    j = j / 2;
    i = i + 1;
  }
  return i;
}

I come up with the following loop invariant:

j >= 0 and i >= 0 must be true before, during and after each iteration.

For case where x >= 0, upon checking the condition the first time, the loop invariant holds true.

For case where any input x >= 0, the invariant loop also holds true.

However, going through some of the other loop invariant reads found here on stackexchange, I am convinced that this is not the loop invariant for this particular algorithm as it does not solve the problem we are trying to accomplish. More specifically, this loop invariant holds true, but without pointing out explicitly that this is a logarithm calculator, the loop invariant is invalid.

I am unsure of the loop invariant I provided as I don't even think it is sufficient for proving out the correctness of the algorithm. How would I create an effective loop invariant that will satisfy the simple algorithm above?

Answer 1

Your understanding is mostly correct. That is a valid loop invariant. It's just a relatively weak one. It is common to find a situation like this, where there are multiple possible loop invariants, some more useful than others. You've found a relatively weak (less useful, less informative) loop invariant.

Your real question is: how do I find a loop invariant that is strong enough to let you prove your code is correct? The answer to that is that you need to start by specifying what it means for your code to be correct. You need to start by writing a specification for your code, that outlines what it means for it to correctly compute the log function.

The specification will typically take the form of a precondition and a postcondition on the function itself. The loop invariant is only a tool to help you prove that the code of log meets the specification for log.

I can't tell you what the right specification is, as you haven't told us what you want log to do. But here is one example specification:

• Precondition: $x=2^k$ for some $k \in \mathbb{N}$

• Postcondition: if $x=2^k$, then the return value of log is equal to $k$

When you try to crank through a Hoare-style proof that log meets this specification, you'll find that you need a loop invariant. The following loop invariant will be sufficient:

$$i \ge 0 \land j \ge 1 \land j = x \cdot 2^i.$$

I don't expect it to necessarily be obvious that this is a valid loop invariant, nor that this is sufficient to prove the code above meets the spec I gave. Fortunately, there is a systematic step-by-step way to verify that: you use Hoare logic. To learn about this, I recommend that your next step be to spend some quality time with a textbook that explains preconditions, postconditions, loop invariants, and Hoarse logic.

Of course, that's not necessarily the only specification you might have in mind. Another possible specification would be

• Precondition: $x \ge 1$

• Postcondition: if $2^k \le x < 2^{k+1}$, then the return value of log is equal to $k$

or even:

• Precondition: $x \ge 1$

• Postcondition: the return value of log is equal to $\lfloor \lg x \rfloor$

Those might require different, more elaborate loop invariants. The point is: whether a loop invariant is strong enough depends upon what you're trying to prove, and in particular, what spec you're trying to prove the code meets.

---

A small correction: When you write

"without pointing out explicitly that this is a logarithm calculator, the loop invariant is invalid",

that's not quite right: the loop invariant you gave is a valid loop invariant. It's just a relatively weak one.

Also, when you write "satisfy the simple algorithm above", that's probably not the right way to put things. I've never heard the word "satisfy" used in this way before. Instead, the right question to ask is: how do I prove that this code meets a particular specification? To ask that, you first need to know what the specification that you're trying to meet is.

Answer 2

Assume input $x \ge 1$, and $x$ is an integer.

Loop invariant: $j*2^i \le x < (j+1)*2^i$, or $[x/2^i]=j$

Proof:

• Initial: $i=0, j=x, x=j*2^i$
• Inducing: Suppose after $k_{th}$ loop, we have $j*2^i \le x < (j+1)*2^i$. After the next loop, $j_1=[j/2]$, $i_1=i+1$, then $j_1*2^{i_1} = [j/2]*2^{i+1} = 2*[j/2]*2^i$, and $(j_1+1)*2^{i_1} = ([j/2]+1)*2^{i+1} = (2*[j/2]+2)*2^i$. Applying $0 \le j-2*[j/2] \le 1$, we have $j_1*2^{i_1} \le j*2^i \le x$ and $(j_1+1)*2^{i_1} \ge (j+1)*2^i \gt x$
• Final: $j=1$, thus $2^i \le x < 2^{i+1}$, ie. $[\log_2x]=i$

Conclusion:log(x) computes the base 2 logarithm of x, rounding down to integer.