Understanding Log(n) Loop Invariant
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 &lt; 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.