问题标签 [loop-invariant]

我有一个数组“line”，其中包含一个长度为“l”的字符串，还有一个数组“nl”，其中包含一个长度为“p”的字符串。注意：“l”和“p”不一定是每个对应数组的长度。参数“at”将是在“line”内进行插入的位置。恢复：长度为“p”的数组将插入“line”，将“line”的所有字符在位置（at，i，at+p），'p'位置之间向右移动以进行插入。

我的确保逻辑是检查插入“line”中的元素是否具有相同的顺序并且是否与“nl”中包含的字符相同。

这是代码：

这是 我收到的错误。

谢谢。

我看到了一个示例程序，它将数组中的每个值都设置为 0：

它表示循环不变量的一部分是0<=i<n. 但是，循环结束后，i 将等于 n。我是否正确地说这不是循环不变量的一部分？如果是这样，它应该用什么代替？完整的不变量是For All j (0<= j < i --> a[i] = 0) & 0 <= i < n)

考虑以下循环：

我想得出结论 y = b ^a

我一直在思考一段时间，似乎无法找出一个足够强大的循环不变量来让我得出结论。有谁知道如何解决这个问题？

非常感谢任何帮助或见解。

我是逻辑世界的新手。我正在学习 Hoare Logic 和程序的部分和全部正确性。我尝试了很多解决以下问题但失败了。

我的一位朋友给了我以下答案，但我不知道它是否正确。

请一步一步教我如何解决这个问题。

更新

解决一些愚蠢问题的问题，下面用给定的类和相应的方法进行描述。如果您需要其他东西，请告诉我，提前谢谢。此外，该链接已使用rise4fun 中的所有这些代码进行更新。

在rise4fun

我总是想知道如何证明一个简单程序的正确性。例如，像First Missing Positive这样的面试问题。该程序如下所示：

如何构造这个程序的不变量？构造简单算法的不变量的一般技巧是什么？

线性搜索循环的伪代码：

我写的循环不变量：

在 for 循环的每次迭代开始时，j是A[j-1]不等于v之后的下一个索引。

初始化：

当j等于1并且在检查它是否小于A.length之前，前一个索引是0。那么A[0]不等于v，因为在这种情况下A[0]甚至不存在。

维护：

如果A[j]等于v则循环终止。这意味着我们没有下一次迭代。但是如果它不等于v那么循环的下一次迭代将在保持循环不变性的同时执行。

终止：

导致 for 循环终止的条件是j大于A.length或v等于A[j]。因为每次循环迭代都将j增加1，所以我们检查了A 的每个元素对v直到j大于A.length。因此算法是正确的。如果v等于A[j]那么这意味着我们已经找到了我们一直在搜索的元素。因此算法是正确的。

这些是正确的吗？

我们知道循环变体被定义为在循环的每次迭代之前和之后都为真的语句。但是这个定义是不是太宽松了？让我们看一个具体的例子：线性搜索。

输入：一个由 n 个数字组成的序列 A = (a ₁ , a ₂ , a ₃ , ..., a _n ) 和一个值 v

输出：一个索引 i 使得 v = A[i] 或 NIL 如果在 A 中找不到 v

这是我的伪代码：

因此，一个典型的循环不变量是（因为我们是从左到右搜索）v 不在当前索引的左侧，或者在数学上，P: ∀p ∈ {1, 2, ..., i - 1}, A[p] ≠ v.这显然是正确的，即使在开始时也是如此，因为 p ∈ Ø 是假的，这使 P 为真，记住每一个全称量化的陈述都可以被认为是一个条件陈述。（但非正式地认为它更容易：开始时，v 的左侧什么都没有。）

我们还可以使用限制较少的条件语句。在这种情况下，Q: If A[i] = v, then 1 ≤ i ≤ n.显然，如果找到 v，这是正确的。如果未找到 v，则 A[i] = v 为假，Q 变为真，无论 i 的值如何。如果我们将算法更改为从右到左搜索，Q 也是正确的。

也许我们希望限制更少。使用始终正确的陈述怎么样？R: Either A[i] = v or A[i] ≠ v.R 在循环的每次迭代之前和之后都成立。

哪些语句 P、Q 和 R 可有效用作循环不变量？

这是知道元素数量的算法