Java loop invariant

int logarithmCeiling(int x) {
    int power = 1;
    int count = 0;

    while (power < x) {
        power = 2 *power;
        count = count +1;
    }
    return c开发者_JS百科ount;
}

The code above is meant to be a method in Java for computing and returning the lower logarithm of a given positive integer using a while-loop. How would I provide an invariant for the loop above? i.e. that holds before it starts, every time the loop body ends, and the negation of the loop condition.

power always equals 2^count at the beginning and end of the loop. For the negation, when the loop is over, x <= power = 2^count.

There's a simple relationship between the value of power and the value of count: power=2^count. This holds at the start and end of the loop, but not at certain places in in the loop body.

Look for variables or conditions that are always true. Each iteration count is always incremented by 1, and power is always multiplied by 2. Since the purpose of the function is to find the lower logarithm of the given argument, you could say the loop invariant is that count is always equal to the logarithm of x, rounded down. Another one would be that count is always equal to the logarithm of power.

I guess you are looking for an invariant which is suited to proof partial correctness of the method? Otherwise "true" or "false" are always invariants. I'd go with something like this:

I: {(power <= x) AND (power == 2 ^ count) AND (x > 2 ^ count -1) AND (power >= 1)}

The r.h.s. can be implied from your initializations and helps ensureing the lower bound for x. Together with the negated loop condition you can later imply.

{(x <= 2 ^ count) AND (x > 2 ^ (count -1))}

which is exactly what you want for showing partial correctness of the whole function.