你如何从函数中推导出循环不变量？

Question

这个函数的循环不变量是什么，你是如何从函数中推导出来的？

我一直在阅读算法，为进一步的研究做准备，但我无法理解如何推导循环不变量。

function maxint(a)
b = 1
c = 1

while b != a
    c = c * 2 + 1
    b = b + 1
end while

return c

Answer 1

循环不变量是在整个循环中不会改变的变量、条件等。找到不变量的要点是找出哪些不变量每次在循环中 accessed/assumed 时都不需要 recomputed/reloaded/reestablished。

不变值是那些在整个循环中都不会改变的值，另一方面，不变条件通常更多地与正确性有关，比如确保不同的线程没有修改循环正在遍历的数据结构.然而，到那时，您可能会说 invariant 是一个有点过载的术语。在这种情况下，您似乎只是追求不变值。

~~因此，如果您正在寻找循环不变值，它们将是 a、2、1 和第二个 1.~~

编辑：

我现在明白这不是一个实际的编程问题；这是一个计算机科学问题，可能属于 CS SE。话虽如此，我想我可以提供帮助。 this 站点上的第 1 步是您应该开始的地方。

总结一下：

将循环转换为更熟悉的 for 循环。
运行手动迭代几次。
尝试找到一种模式，为您提供 return 值的公式，该公式不是根据 return 值递归定义的。您希望它仅取决于当前迭代计数和循环中使用的其他 variables/values。

步骤 1

请注意，代码可以转换为以下 for 循环：

c = 1
for (b = 1; b <= a; b = b + 1)
    c = c * 2 + 1
end for

现在，我们可以看到b只是循环变量，a是循环边界。为了使事情更清楚，我们可以将其写成更传统的 c 风格 for 循环：

c = 1;
for (i = 1; i <= n; i++) {
    c = c * 2 + 1;
}

第 2 步

i_0: c =     ?      = 1 // Don't forget the initial value! Call that iteration 0.
i_1: c = 1  * 2 + 1 = 3
i_2: c = 3  * 2 + 1 = 7
i_3: c = 7  * 2 + 1 = 15
i_4: c = 15 * 2 + 1 = 63

步骤 3

在其中寻找将输出变量 c 与当前迭代 i 相关联的模式。

请注意，此上下文中的 i 指的是循环的当前迭代，而不是代码中变量 i 的值。

注意出现了 2 的幂模式：c_i = 2^(i+1) - 1。

事实上可能不止一个出现。我们怎么知道这个是否有效？这就是基本迭代和归纳步骤的目的。

为迭代插入 0 给我们 c_0 = 2^(0+1)-1 = 2-1 = 1，这给了我们 c 的起始值，所以很好。

对于归纳步骤，我们需要证明c_(i+1) = 2^(i+2) - 1。问题是，我们不能说完就收工了。我们需要 c_(i+1) 等于的其他东西。

幸运的是，这正是代码给我们的，一个计算新值 c 的公式，给定上一次迭代的值：c = c * 2 + 1，正式写成：

c_(i+1) = c_i * 2 + 1。

我们假设我们的不变量是正确的，并将其插入 c_i。然后，我们将整个事情设置为 2^(i+2) - 1:

c_(i+1) = (2^(i+1) - 1) * 2 + 1 = 2^(i+2) - 1。

(2^(i+1) - 1) * 2 + 1 = 2*2^(i+1) - 2 + 1 = 2^(i+2) - 1

我们满足了基本情况和归纳步骤，所以我们知道我们的不变量是正确的。我们还表明，由于循环在迭代时终止 n, c = 2^(n+1) - 1.

TL;DR

代入原变量：

循环不变量：c = 2^(b+1) - 1.
maxint(a): 2^(a+1) - 1

你如何从函数中推导出循环不变量？

How do you derive a loop invariant from a function?

proof-of-correctness

步骤 1

第 2 步

步骤 3

TL;DR