algorithm - 这个循环不变量及其非正式证明是否正确？ (CLRS 第三版练习 2-1-3)

Question

给定以下线性搜索算法(将索引 1 称为元素数组中第一个元素的索引):

found_idx = nil
for i = 1 to A.length
  if A[i] == value
    found_idx = i
    return found_idx
  end-if
end-for
found_idx

我想知道这个循环不变式是否正确: “在 for 循环的每次迭代开始时，found_idx 是数组中以 i-1 结尾的索引，如果该值存在，则该值存在”

这是我根据 CLRS 中的格式提出的对此循环不变性的非正式解释:

1. 初始化:在第一次迭代之前为真，因为 i = 1 并且以 i-1 结尾的数组为空，因此 found_idx 为 nil。
2. 维护:每次迭代后都是如此，因为在 i 的每个值处，检查 A[i] 并然后 i 递增，这意味着在每次新迭代之前检查了直到 i-1 的所有元素。
3. 终止:当 i > A.length 时终止，这意味着已经检查了直到并包括 A.length 的所有元素。

我主要担心的是，引用以 i-1 结尾的索引感觉不正确，因为循环从 i 的 1 开始，这是第一个数组的元素。换句话说，引用数组的子数组感觉很荒谬，其中子数组结束于小于数组起始索引的索引，子数组首先应该是子数组。这似乎暗示上面给出的循环不变量在循环的第一次迭代之前实际上是假的。

想法？

Answer 1

由于循环提前终止，其不变量如下:

found_idx = nil && ∀k<i : A[k] ≠ value

&&之后的部分意思是“所有 A 的元素在 i 下面的索引不等于 value”。

• 在进入循环之前这是平凡的事实
• 有条件的要么保留found_idx在 nil , 或者提前终止循环
• 当 i 时循环终止达到 A.length

循环的后置条件是found_idx = nil && ∀k<A.length : A[k] ≠ value ，这仅仅意味着 value不在A之中的元素。这也意味着您可以消除 found_idx通过如下重写循环:

for i = 1 to A.length
    if A[i] == value
        return i
    end-if
end-for
return nil