问题标签 [loop-invariant]

我编写了自己的琐碎小函数（为方便起见是 php），并希望有人可以通过归纳来帮助构造一个证明，这样我就可以掌握它的一个非常基本的窍门。

结果是每个索引处的值与索引本身相同，但这只是因为 a[0] 被初始化为 0。

我相信目标是（或应该是）证明不变量（它本身可能是可疑的，但希望能得到理解）适用于 k+1。

谢谢

编辑：示例：http ://homepages.ius.edu/rwisman/C455/html/notes/Chapter2/LoopInvariantProof.htm

我正在学习数据结构和算法的基础课程，我们使用的书是 CLRS 的开创性著作。我在理解循环不变量时遇到了一些麻烦，如第 2.1 章所述：插入排序。

书上说：

在第 1-8 行的 for 循环的每次迭代开始时，子数组 A[1..j -1] 由最初在 A[1..j-1] 中的元素组成，但按排序顺序。

现在，这让我很困惑。为什么在第一次迭代开始时会保持这种状态？假设要排序的数组看起来像 { 5, 2, 4, 6, 1, 3 }。现在，当 for 循环的第一次迭代开始时，A[1.. j-1] 不是按排序顺序排列的，但当迭代结束时它是有序的。

我在这里想念什么？

这是过去试卷中的一道题。

为什么i<=n循环测试说循环不变量说i<n。

是一个合适的答案：它说i<=nas iwill equaln在 while 循环的失败条件下。因此，第 6 次迭代i将等于n失败条件下的值 6。但是，while 循环本身状态i<n为i从 0 开始，并且将完成循环一次i等于 5。

我想知道循环不变量。我开始知道在算法（主要是排序算法）中有一个循环不变量，循环不变量表示算法的正确性。

这是如何运作的？有人可以帮助我理解这一点吗？

我将如何获得循环不变量并为以下算法证明它。

我无法证明 2 个循环不变量：

我猜 \at 不像我预期的那样适用于数组。

ACSL by Example中有一个类似的函数（第 68 页，swap_ranges），它使用了这个，但是，如前所述，他们无法用 WP 插件证明这个特定的函数。我在我的机器上尝试过，确实无法证明相同的不变量。

完整代码

编辑

我使用 Frama-C Oxygen 版本并尝试使用 alt-ergo(0.94) 和 cvc3(2.4.1) 进行自动证明

frama-c 的输出：

cvc3:

交替：

有人可以为以下简单算法提供一个可能的循环不变量：

输入：A[0,...,n-1]和B[0,...,m-1]，每个都可能包含重复的元素

输出：第一对 (i,j) 使得A[i] == B[j].

算法：

到目前为止，我只有一种可能有效或无效的解决方案：

S = {(i,j) | A[0,...,i-1] and B[0,...,j-1] has no common elements}

我遇到了一个问题，提出了后置条件并显示了这段代码的部分正确性。

我不是在寻找答案，因为这是学校的作业，只是洞察力，也许是一些指向正确方向的东西。我已经构建了值表，并且无法提出循环不变量。

我知道循环的结果是 m 后面的完美正方形，但我不确定如何写。

一如既往，感谢所有帮助。

我试图找到循环的不变量（例如在下面的代码中）我真的不知道如何找到一般的不变量。任何人都可以帮助我如何找到一个不变量，并帮助我找到它的以下代码？谢谢

我对不变量有点熟悉，我或多或少可以在一个小循环中找到它。在为以下 java 伪代码求解不变量时，我感到很困惑。谁能帮忙：