这个循环不变式及其非正式证明是否正确？（CLRS 第 3 版练习 2-1-3）答案

【问题标题】：Is this loop invariant and its informal proof correct? (CLRS 3rd ed. exercise 2-1-3)这个循环不变式及其非正式证明是否正确？（CLRS 第 3 版练习 2-1-3）
【发布时间】：2018-02-14 13:51:35
【问题描述】：

给定以下线性搜索算法（将索引 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 中的格式对这个循环不变量提出的非正式解释：

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

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

想法？

【问题讨论】：

现在found_idx 没用了：您可以将return i 放在中间，然后完全删除found_idx，因为分配了found_idx 的循环永远不会到达末尾。
如果在数组中没有找到值，那么循环将结束，不是吗？
对，在这种情况下，found_idx 将保持为nil。
是的，这就是目的。那么，我提出的循环不变量可能存在几个问题？我更关心如何构造适当的循环不变性并随后正确使用它，而不是伪代码的优雅或简洁

标签： algorithm search clrs loop-invariant

【解决方案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

【讨论】：