问题标签 [loop-invariant]

我试图找到一个循环不变量，以便我们可以证明这个程序部分正确：

我真的被困住了。到目前为止，我尝试过的一些不变量是：

和

我真的很感激一些建议。

我已经阅读了多篇文章，包括 Jon Bentley 关于二分搜索的章节。这就是我对正确二进制搜索逻辑的理解，它适用于我所做的简单测试：

现在要找到第一次出现的排序重复项，如果条件继续而不是返回 mid 作为

类似地，要获得重复元素的最高索引，low = mid + 1如果arr[mid]==k

这个逻辑似乎有效，但在多个地方我看到循环不变量为

我很困惑，想了解您何时可能想要使用low + 1 < high而不是low < high.

在我上面描述的逻辑中，low + 1 < high如果您使用简单的示例进行测试，则会导致错误。

有人可以澄清为什么以及何时我们可能想要low + 1 < high在 while 循环中使用而不是low < high？

我正在尝试了解 C 中的循环不变量。我有一个代码并且我有循环不变量，但我不完全理解为什么。这是代码：

循环不变量是： 0 < m < n < ASIZE OR m == n OR m == n+1

我想我理解 0 < m < n < ASIZE。这将是因为 while 循环，它说 m 不能为 0，但它必须小于 n。并且 n 必须小于数组大小。

但我不明白为什么 m == n 和 m == n+1。

有什么想法吗？

我需要为给定的一段代码想出一个循环不变量：

我的不变量是：

这是一个混乱的不变量，我不能 100% 确定它是正确的。是否有更好的不变量可以覆盖 z = x^y 的后置条件

我试图在以下代码中找到循环不变量：

查找最接近的对 Iter(A) ：

我认为循环不变量是 min = Distance(A[i],A[j]) 所以 A 中最近的点是 A[p] 和 a[q] 。我试图证明程序的正确性。在这里，我想通过让 i 成为一些常数来证明内循环，然后一旦我证明了内循环，就用它的循环不变量替换它并证明外循环。顺便说一句，这是家庭作业。任何帮助都感激不尽。

我无法理解如何找到循环不变量并为它们编写正式的语句。因此，循环不变量只是在循环的每次迭代之前和之后立即为真的条件。看起来代码正在执行交换：如果数组中的以下元素大于当前元素，则切换位置。我的意思是从循环不变量的定义来看，它听起来真的是 i < 100 因为循环运行必须是这样，但我不太明白。非常感谢一些澄清。

我试图找到这段代码的循环不变量。通常我实际上会通过输入来检查代码并尝试找出答案。但这种方法并不总是奏效。只是想知道是否有更好的方法来找到循环不变量？任何建议将不胜感激！

其中'a'是一个整数数组。我正在做一个问题文件，它问我这是什么循环不变量，我已经确定代码可以确定数组是否包含 0。但到目前为止，我只能认为不变量是

并且问题状态包括变量 i、a 和 answer 在不变量中，所以我知道这不可能是正确的。我之前没有遇到过涉及布尔值的循环不变量并且很困惑，有人可以帮忙解释一下吗？

给定以下代码片段，其中 x 是一个数字。

它计算什么？证明它，展示如何推导出循环不变量。

请问我该怎么做？

我不太明白如何确定循环不变量。我知道它在循环之前、循环之后和每个循环迭代期间都是正确的，但仅此而已。这是我正在处理的一个示例问题，您如何找到这个循环不变量？