theory - 如何选择和设置正确的循环不变量？

Question

我遇到了以下有关循环不变量的问题:

考虑

x=4;
for(i=5;i<k;i++) {
a=a+x+i;
x=x*2;
}

定义适当的循环不变量，利用 a 和 x 的闭合公式。

现在，你怎么知道这里有正确的循环不变式？我的意思是你可以将循环不变式设置为:“在第 j 次迭代时，'x' 小于 'a'”，这是正确的，但不会使用任何封闭公式，对吗？

当循环结束时，如何使用语句(循环不变式)来确定“a”的值？我见过的所有示例都只是说明循环不变式，并且它不被用作封闭公式。

有什么想法吗？

感谢您的帮助。

Answer 1

从封闭公式开始:显然，对于 x(j) [对于 j 从 0 到 k-5]，x 在循环第 j 段的入口处，x(j+1) = x (j) * 2，因此，x(j) 为 4 * 2**j(使用 ** 表示“上电”)，因为 x(0) 是 4；和 a(j+1) = a(j) + x(j) + j + 5 ——我们不知道 a(0) 是什么，但是我们可以将其分解出来并将 a(j) 写为 a(0) + 某物。考虑到上述 x(j) 的封闭公式结果，你能算出那东西是什么吗？我舍不得给你做作业——你开始学习了吗Concrete Mathematics或者无论你的教科书是什么......？

一旦您写下了 a(j) 的封闭式公式，请与我为 x(j) 提供的简单公式配合使用，您可以吗看看它们如何组合起来使循环不变......？