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

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 都是奇数，就像它们在我的示例中一样，那么我的 Loop 不变量是正确的(至少看起来是这样)

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

< 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'th迭代结束时(i从1开始)，y保持2^i的事实，所以y - 1 == 2^i - 1是一个二进制表示为i1位的数字(即11...11i位)。当你用b&这个数字时，你会得到bi最低有效位。