1

给定以下线性搜索算法（将索引 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. Termination：这在 时终止i > A.length，这意味着所有元素A.length都已被检查。

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

想法？

4

1 回答 1

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
于 2018-02-14T14:28:06.130 回答