java - Java 循环不变量

Question

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

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

上面的代码是 Java 中的一种方法，用于使用 while 循环计算和返回给定正整数的下对数。我将如何为上面的循环提供不变量？即在它开始之前，每次循环体结束时，以及循环条件的否定都成立。

Answer 1

power 在循环的开始和结束时总是等于 2^count。对于否定，当循环结束时，x <= power = 2^count。

Answer 2

power的值和 的值之间有一个简单的关系count： power=2 ^count。这适用于循环的开始和结束，但不适用于循环体中的某些位置。

Answer 3

我猜您正在寻找适合证明该方法的部分正确性的不变量？否则“真”或“假”总是不变的。我会用这样的东西：

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

rhs 可以从您的初始化中暗示出来，并有助于确保 x 的下限。与否定循环条件一起，您可以稍后暗示。

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

这正是您想要显示整个函数的部分正确性的内容。

Answer 4

寻找始终为真的变量或条件。每次迭代计数始终递增 1，幂始终乘以 2。由于该函数的目的是找到给定参数的下对数，因此您可以说循环不变量是计数始终等于x，四舍五入。另一个是计数总是等于幂的对数。