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

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

Answer 2

power 的值和 count 的值之间存在一个简单的关系：power = 2^计数。这在循环的开始和结束时成立，但在循环主体中的某些位置不成立。

Answer 3

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

Answer 4

我想你正在寻找一个适合证明方法部分正确性的不变量？否则，"真"或"假"总是不变的。我会选择这样的东西：

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

r.h.s. 可以从您的初始化中隐含出来，并有助于确保 x 的下限。连同否定循环条件，您可以稍后暗示。

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

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