循环线性搜索的不变量

Question

如算法简介(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之间).非常感谢提前!

Answer 1

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

循环不变式：在循环的i第 1 次迭代开始时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按预期结束。

Answer 2

看了索引之后i,还没有找到v,v关于数组之前i和之后关于数组部分的部分你能说些什么i？

Answer 3

在线性搜索的情况下,循环变体将是用于保存索引(输出)的后备存储.

让我们将后备存储命名为索引,该索引最初设置为NIL.循环变量应符合以下三个条件:

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

.

Answer 4

循环不变将是

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

循环终止：

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

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

正确性证明：留作练习