线性搜索的循环不变量

如算法简介（http://mitpress.mit.edu/algorithms）所示，练习陈述如下：输入：数组A [1 ... n] 输出：i，其中A [i] = v或未找到时为NIL 为LINEAR-SEARCH写一个伪代码，扫描序列，寻找v。使用循环不变量，证明你的算法是正确的。（确保你的循环不变完善了三个必要的属性 - 初始化，维护，终止。）我没有创建算法的问题，但我没有得到的是我如何决定我的循环不变量。我认为我理解了循环不变量的概念，即在循环开始之前，在每次迭代的结束/开始时始终为真的条件，并且当循环结束时仍然为真。这通常是目标，例如，在插入排序时，迭代j，从j = 2开始，[1，j-1]元素始终排序。这对我来说很有意义。但对于线性搜索？我想不出任何东西，想到循环不变只是听起来太简单了。我明白了什么问题吗？我只能想到一些明显的东西（它是NIL或介于0和n之间）。非常感谢提前！

已邀请:

7 个回复

秃拳割

你看了索引i，还没找到v，关于i之前的数组部分和关于i之后的数组部分，你能说一下v？

盛虱

在线性搜索的情况下，循环变体将是用于保存索引（输出）的后备存储。让我们将后备存储命名为索引，该索引最初设置为NIL。循环变量应符合以下三个条件：初始化：这个条件适用于索引变量。因为它包含NIL，它可能是结果，在第一次迭代之前是真的。维护：索引将保持NIL，直到找到项目v。在迭代之前和下一次迭代之后也是如此。因为，在比较条件成功之后，它将在循环内设置。终止：索引将包含NIL或项目v的数组索引。。

埠仙俊

循环不变将是 forevery 0＆lt; = i＆lt; k，其中k是循环迭代变量的当前值， A [i]！= v 循环终止：如果A [k] == v，则循环终止并输出k 如果A [k]！= v，并且k + 1 == n（列表大小），则循环终止，值为nil 正确的证据：留作练习

好按紊叉

LINEAR-SEARCH(A, ν)
1  for i = 1 to A.length
2      if A[i] == ν 
3          return i
4  return NIL

循环不变：在for循环的第0次迭代开始时（第1-4行），

∀ k ∈ [1, i) A[k] ≠ ν.

初始化：

i == 1 ⟹ [1, i) == Ø ⟹ ∀ k ∈ Ø A[k] ≠ ν,

这是真的，因为关于空集的任何陈述都是真的（真空）。维护：假设在for循环的第0次迭代开始时循环不变量为真。如果A[i] == ν，则当前迭代是最后一次（参见终止部分），因为第3行被执行;否则，如果A[i] ≠ ν，我们有

∀ k ∈ [1, i) A[k] ≠ ν and A[i] ≠ ν ⟺ ∀ k ∈ [1, i+1) A[k] ≠ ν,

这意味着不变循环在下一次迭代开始时仍然为真（i+1）。终止：for循环可能因两个原因而结束： return i（第3行），如果A[i] == ν; i == A.length + 1（for循环的最后一次测试），在这种情况下，我们处于A.length + 1迭代的开始，因此循环不变量是

∀ k ∈ [1, A.length + 1) A[k] ≠ ν ⟺ ∀ k ∈ [1, A.length] A[k] ≠ ν

并返回NIL值（第4行）。在这两种情况下，LINEAR-SEARCH都按预期结束。

纫合峭

假设您有一个长度为i的数组，索引自[0 ... i-1]，算法正在检查此数组中是否存在v。我不完全确定，但我认为，循环不变量如下：如果j是v的索引，那么[0..j-1]将是一个没有v的数组。初始化：在从0..i-1迭代之前，检查当前数组（无），不包括v。维护：在j处找到v时，来自[0..j-1]的数组将是没有v的数组。终止：当循环在j处找到v时终止，[0..j-1]将是没有j的数组。如果数组本身没有v，那么j = i-1，上述条件仍然适用。

谷起

我写的LS算法是 -

LINEARSEARCH(A, v)
  for i=0 to A.length-1
    if(A[i] == v)
      return i
  return NIL

我为循环不变量做了我自己的假设来检查线性搜索的正确性.....也许它完全错了所以我需要对我的假设提出建议。 1）在初始化时 - 在i = 0时，我们在i = 0处搜索v。 2）在连续的迭代中 - 我们正在寻找v直到i＆lt;则为a.length-1 3）在终止时，i = A.length，直到A.length，我们一直在寻找v。

膛嵌墒缅欠

线性搜索的不变量是i之前的每个元素都不等于搜索关键字。二进制搜索的合理不变量可能是[低，高]范围，低值之前的每个元素都小于键，高位之后的每个元素都大于或等于。请注意，二元搜索有一些变体，其不变量和属性略有不同 - 这是“下界”二进制搜索的不变量，它返回等于或大于键的任何元素的最低索引。来源：HTTPS：//www.reddit.com/r/compsci/comments/wvyvs/what_is_a_loop_invariant_for_linear_search/ 对我来说似乎是对的。

要回复问题请先登录或注册

线性搜索的循环不变量

7 个回复

发起人

invariants

loop_invariant

问题状态

线性搜索的循环不变量

与内容相关的链接

7 个回复

发起人

invariants

loop_invariant

问题状态