计算阶乘的函数的循环不变式

Question

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。

这就是我的困惑所在。有些书籍文章指出循环不变式是一个必须在循环开始时（即前置条件）和循环结束时（即后置条件）都成立的语句，但不一定需要在循环过程中始终成立。

以上函数的正确循环不变式是什么？

- Brownbay

2

循环不变式并非后置条件。任何声称如此的阅读材料都是完全错误的。如果你找到了一些暗示循环不变式也是后置条件的内容，请包含一个链接或参考资料。这是不完整或误导性的。循环不变式而不是while条件是后置条件。 - S.Lott

我猜我肯定误读了作者的陈述。我正在阅读Susanna Epp的“应用离散数学”，我假设循环不变量是预/后条件的组合，而似乎作者的意思是循环不变量也只是确保预/后条件的真实性。 - Brownbay

作者的意思是循环不变式也确保了前/后置条件的真实性。鉴于这种修正的理解，请更新您的问题以寻求您真正需要的帮助。 - S.Lott

2个回答

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显然可以轻松实现这一点。但在许多实际的循环中并不明显，所以你必须问问自己的循环设计这个问题。）

- S.Lott

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- sth · Accepted Answer

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

循环开始前必须满足先决条件，循环结束后必须满足后置条件，而不管循环已经进行了多少次迭代，不变量必须保持不变（这就是为什么它被称为“不变量”——它不会改变真实性）。

通常，同一个循环可能有不同的可能不变量。例如，1 = 1将作为任何循环的真实不变量，但是要证明算法的正确性，通常需要找到更强的不变量。