3

我很难正确识别以下函数的循环不变量：

F(y)
    X <-- 1
    while (y > 1)
        do x <-- x * y
           y <-- y - 1
    return (x)

我已经确定循环不变量是x = 1 OR x = y!因为该语句作为前置条件成立并且作为后置条件成立。

它似乎并不适用于每次迭代，例如如果 y = 3，那么在循环的第一次迭代中，x = 1 * 3 等于 3 而不是 3！相当于 6。

我想这就是我真正困惑的地方。一些书籍文章指出，循环不变量是在开始或循环时必须等于真（因此是前置条件）并且在循环结束时也必须为真（因此是后置条件）但不一定需要的语句在循环的中途保持真实。

上述函数的正确循环不变量是什么？

4

2 回答 2

6

一个可能的循环不变量是x⋅y！= y 0！其中y 0是传递给函数的y的初始值。无论循环已经完成了多少次迭代，这句话总是正确的。

前提条件必须在循环开始之前保持，后置条件必须在循环结束后保持，并且无论循环进行了多少次迭代，不变量都必须保持（这就是为什么它被称为“不变量” - 它没有' t改变它是真的）。

通常，同一循环可能有不同的可能不变量。例如1 = 1作为任何循环的不变量都是正确的，但要显示算法的正确性，您通常必须找到更强的不变量。

于 2011-12-05T23:39:15.393 回答
1

循环不变量可以从后置条件、一点直觉和一些类似代数的推理中推导出来。

您知道后置条件的一部分：x == Y!，其中Y作为参数给出的初始值。 y是一个值变化的变量。这就是后置条件的其余部分，顺便说一句：y == 1。

每次传递的真实情况是什么？向后推理。

在最后一关x == Y*Y-1*...*2 and y == 2。

在那之前？ x == Y*Y-1*...*3 and y == 3.

在那之前？

什么时候是真的，什么时候y == Y？

最后。给定后置条件和不变量，启动事物所需的最弱语句集是什么前置条件？代码表明，x=1 and y=Y.

您知道，每次通过循环时，都必须发生一些变化，并且程序必须可证明地将状态推进到后置条件。真的吗？是否存在循环状态的自然值函数可证明向零减小？（这似乎是一个棘手的问题，因为y变量似乎很容易做到这一点。在许多现实世界的循环中并不明显，所以你必须问你的循环设计问题。）

于 2011-12-06T01:00:07.490 回答