java - 努力寻找正确的循环不变量

Question

我有以下代码:

public static void main(String[] args) {
    int a = 3;
    int b = 7;

    int x = b; // x=b
    int res = a; // res = a
    int y = 1;

    int invariant = 0;

    System.out.println("a|b|x|y|res|invariant");
    while (x > 0) { 
        if (x % 2 == 0) {
            y = 2 * y;
            x = x / 2;  
        } else {
            res = res + y;
            y = 2 * y;
            x = (x - 1) / 2;
        }
        invariant = y + 2;
        String output = String.format("%d|%d|%d|%d|%d|%d", a,b,x,y,res,invariant);
        System.out.println(output);
    }
    // < res = a + b >
}

输出如下:

a|b|x|y|res|invariant
3|7|3|2|4|4
3|7|1|4|6|6
3|7|0|8|10|10

但是，如果我更改数字，则不变量不再等于 res。因此，这个问题的循环不变式是不正确的。

我正在努力寻找正确的循环不变式，如果有人可以给我任何提示，我会很高兴。

查看代码和结果后，我的第一印象是循环不变式根据 a 和 b 变化。假设 a 和 b 都是奇数，就像我的示例中一样，那么我的循环不变量是正确的(至少看起来是这样)

假设如下所示的循环变体是否正确？

< res = y - 2 && a % 2 != 0 && b % 2 != 0 >

我确实使用了不同的数字，似乎每当我更改它们时都会出现不同的循环不变量，并且我很难找到任何模式。

如果有人能给我关于如何解决这个问题的提示或一般想法，我将非常感激。

谢谢

Answer 1

此循环计算总和a+b。res 被初始化为a。然后，在循环的每次迭代中，b 的二进制表示的下一位(从最低有效位开始)被添加到 res 中，直到循环结束并且res 保存 a+b。

它是如何工作的:

x 初始化为 b。在每次迭代中，您都会消除最低有效位。如果该位为 0，则只需将 x 除以 2。如果该位为 1，则减去 1 再除以除以 2(实际上除以 2 就足够了，因为当 x 是奇数 int< 时 (x-1)/2==x/2/)。仅当遇到 1 位时，您必须将其添加(乘以 2 的正确幂)到结果中。 y 保存 2 的正确幂。

在 a=3, b=7 示例中，b 的二进制表示形式为 111

• 在第一次迭代中，res 的值为 a + 1(二进制)== a + 1 = 4
• 在第二次迭代中，res 的值为 a + 11(二进制)== a + 3 = 6
• 在最后一次迭代中，res 的值为 a + 111(二进制)== a + 7 == 10

您可以将不变量写为:

invariant = a + (b & (y - 1));

这利用了以下事实:在第 i 次迭代结束时(i 从 1 开始)， y 包含 2^i，因此 y - 1 == 2^i - 1 是一个数字，其二进制表示为 i 1 位(即 11...11 和 i 位)。当您将此数字与 b 相加时，您将获得 b 的 i 最低有效位。