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

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-1)/2==x/2 当 x 是奇数时 int)。只有当你遇到一个 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 最低有效位。

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

Struggling to find the correct loop invariant

java

assert

loops