Java循环不变式

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

    while (power < x) {
        power = 2 *power;
        count = count +1;
    }
    return count;
}

power

count

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

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