2
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ Welcome to CS.SE! There's no reason you would know this, but this kind of question isn't a good fit for our site. We discourage "please check whether my answer is correct", as only "yes/no" answers are possible, which isn't really helping either you nor future visitors very much. Please read related meta discussions here and here and adjust your question accordingly, e.g. by formulating a specific question about a conceptual issue you are uncertain about. $\endgroup$ – D.W. Aug 25 '15 at 17:44
  • $\begingroup$ To put it another way: What prevents you from answering your question on your own? If you're not sure how to tell whether your answer is correct, is that because of a conceptual gap in your understanding? If so, asking about that might be a better fit -- it might be more likely to yield a question that will be useful to others in the future. If you just need someone to check your work, you can always seek out a friend, classmate, or teacher. As a rule of thumb, a good conceptual question should be useful even to someone who isn't looking at the problem you happen to be working on. $\endgroup$ – D.W. Aug 25 '15 at 17:45
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thank you for the follow up. This helped me understand it a lot more clearer. Originally I had a similar post condition, I may have done something wrong as I was stepping through by plugging in values of n >= 1 which made me revert back to my weak invariant. $\endgroup$ – Cancos Aug 25 '15 at 18:52
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.