algorithm - 线性搜索的循环不变量

Question

如在算法简介 (http://mitpress.mit.edu/algorithms) 中所见，练习说明如下:

输入数组A[1..n]和一个值v

输出索引i，其中A[i] = v or NIL if v 在 A

中找不到

Write pseudocode for LINEAR-SEARCH, which scans through the sequence, looking for v. Using a loop invariant, prove that your algorithm is correct. (Make sure that your loop invariant fulfills the three necessary properties – initialization, maintenance, termination.)

我创建算法没问题，但我不明白的是如何确定我的循环不变量是什么。我想我理解了循环不变性的概念，即在循环开始之前、每次迭代的结束/开始时始终为真并且在循环结束时仍然为真的条件。这通常是目标，例如，在 insertion sort ，遍历 j，从 j = 2 开始，A[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 

循环不变性:在 for 循环的第 i 次迭代开始时(第 1-4 行)，

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

初始化:

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

这是真的，因为关于空集的任何陈述都是真的(无意义的真理)。

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

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

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

终止:for 循环可能由于两个原因而终止:

1. 返回 i(第 3 行)，如果 A[i] == ν;

2. 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 都按预期结束。