34

正如在算法简介 ( 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 之间）。提前非常感谢！

4

7 回答 7

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

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

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

初始化： 

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

这是真的，因为任何关于空集的陈述都是真的（空虚的真理）。

维护：假设循环不变量在循环的i第 th 次迭代开始时为真for。如果A[i] == ν，则当前迭代是最后一次（参见终止部分），执行第 3 行；否则，如果A[i] ≠ ν，我们有

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

这意味着不变循环在下一次迭代（第i+1th）开始时仍然为真。

终止：for循环可能因两个原因而结束：

  1. return i（第 3 行），如果A[i] == ν；

  2. i == A.length + 1（for循环的最后一次测试），在这种情况下，我们处于A.length + 1第 th 次迭代的开始，因此循环不变量是

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

    并NIL返回值（第 4 行）。

在这两种情况下，都LINEAR-SEARCH按预期结束。

于 2018-08-09T14:53:43.013 回答
19

在你查看了 index 之后i，还没有找到，关于数组之前的部分和之后的数组部分v，你能说些什么呢？vii

于 2011-04-07T17:28:13.343 回答
8

在线性搜索的情况下，循环变体将是用于保存索引（输出）的后备存储。

让我们将后备存储命名为最初设置为 NIL 的索引。循环变体应符合三个条件：

  • 初始化：此条件适用于索引变量。因为它包含 NIL，这可能是结果结果，并且在第一次迭代之前为真。
  • 维护：索引将保持 NIL 直到找到项目 v。在迭代之前和下一次迭代之后也是如此。因为，它将在比较条件成功后设置在循环内部。
  • 终止：索引将包含 NIL 或项目 v 的数组索引。

.

于 2016-05-05T06:02:28.070 回答
5

循环不变量将是

永远 0 <= i < k，其中 k 是循环迭代变量的当前值，A[i] != v

循环终止时：

如果 A[k] == v，则循环终止并输出 k

如果 A[k] != v，并且 k + 1 == n（列表大小），则循环以 nil 值终止

正确性证明：留作练习

于 2011-04-07T17:37:00.880 回答
2

假设您有一个长度为 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，上述条件仍然成立。

于 2017-11-17T09:04:10.877 回答
1

线性搜索的不变量是 i 之前的每个元素都不等于搜索键。二分搜索的合理不变量可能是范围 [low, high)，low 之前的每个元素都小于 key，high 之后的每个元素都大于或等于。请注意，二进制搜索有一些变体，不变量和属性略有不同 - 这是“下限”二进制搜索的不变量，它返回等于或大于键的任何元素的最低索引。

来源：https ://www.reddit.com/r/compsci/comments/wvyvs/what_is_a_loop_invariant_for_linear_search/

对我来说似乎是正确的。

于 2017-08-27T17:03:07.223 回答
0

我写的 LS 算法是——

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

我对循环不变量做出了自己的假设，以检查线性搜索的正确性：

  1. 在 Initialisation- at i = 0 处，我们在 i = 0 处搜索 v。

  2. 在连续迭代中 - 我们正在寻找 v 直到 i < A.length-1

  3. 在终止时- i = A.length 直到 A.length 我们一直在寻找 v。

于 2016-08-10T15:42:40.413 回答