问题标签 [loop-invariant]

当使用形式方面来创建一些代码时，是否有确定循环不变量的通用方法，或者它会根据问题完全不同？

我正在阅读 CLRS 的“算法简介”。在第 2 章中，作者提到了“循环不变量”。什么是循环不变量？

什么是循环不变量，如何使用它们来证明堆排序算法的正确性？

我正在查看 Hoare Logic，但在理解查找循环不变量的方法时遇到了问题。

有人可以解释用于计算循环不变量的方法吗？

循环不变量应该包含什么才能成为“有用的”？

我只处理简单的示例，在以下示例中查找不变量并证明部分和完全更正：

正如在算法简介 ( http://mitpress.mit.edu/algorithms ) 中看到的，练习陈述如下：

输入：数组A[1..n]和一个值v

输出：索引i，在哪里A[i] = v或NIL如果v没有找到A

为 LINEAR-SEARCH 编写伪代码，它扫描序列，寻找 v。使用循环不变量，证明你的算法是正确的。（确保你的循环不变量满足三个必要的属性——初始化、维护、终止。）

我创建算法没有问题，但我没有得到的是如何确定我的循环不变量。我想我理解了循环不变量的概念，即在循环开始之前、每次迭代的结束/开始时始终为真并且在循环结束时仍然为真的条件。这通常是目标，例如，在插入排序、迭代j、从 开始j = 2，A[1..j-1]元素总是被排序的。这对我来说很有意义。但是对于线性搜索？我什么都想不出来，想一个循环不变量听起来太简单了。我理解错了吗？我只能想到一些明显的东西（它不是 NIL 就是介于 0 和 n 之间）。提前非常感谢！

上面的代码是 Java 中的一种方法，用于使用 while 循环计算和返回给定正整数的下对数。我将如何为上面的循环提供不变量？即在它开始之前，每次循环体结束时，以及循环条件的否定都成立。

What is the Loop Invariant(s) in this sample code.
This is an excerpt code implemented in C programming language:

These are my initial answers (Loop Invariant):

1. y>=n
2. x<=m
3. z>=0

I am still unsure about this. Thanks.

所以我有这个任务：

我需要关于问题 2 的帮助。

当我意识到阶乘是向后计算的时，我以为我知道该怎么做。该算法直观地是正确的，但我似乎无法找到在循环开始之前成立的循环不变量。

我很困惑。谢谢。

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

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

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

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

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

我不是 100% 确定三次幂求和中的不变量是什么。

注意：n 始终为非负值。

伪代码：

我知道它很乱，可以用更简单的方式完成，但这是我应该做的（主要用于算法分析实践）。

我要提出三个循环不变量；LI1、LI2 和 LI3。
我在想，对于 LI1，不变量与 tot=(i^2(i+1)^2)/4 （从 0 到 i 的平方和的方程）
我不知道要做什么为 LI2 或 LI3 做。LI2 的循环使 i^3 和 LI3 使 i^2，但我不完全确定如何将它们定义为循环不变量。

如果我在每个 while 循环体中都有 3 个单独的总变量，这些变量在第一个循环中 i++ 之前添加到主总数中，那么不变量会更容易定义吗？

谢谢你提供的所有帮助。