1

线性搜索循环的伪代码：

for j = 1 to A.length 
   if(A[j] = v) 
      return j;
return NIL

我写的循环不变量：

在 for 循环的每次迭代开始时，j是A[j-1]不等于v之后的下一个索引。

初始化：

当j等于1并且在检查它是否小于A.length之前，前一个索引是0。那么A[0]不等于v，因为在这种情况下A[0]甚至不存在。

维护：

如果A[j]等于v则循环终止。这意味着我们没有下一次迭代。但是如果它不等于v那么循环的下一次迭代将在保持循环不变性的同时执行。

终止：

导致 for 循环终止的条件是j大于A.length或v等于A[j]。因为每次循环迭代都将j增加1，所以我们检查了A 的每个元素对v直到j大于A.length。因此算法是正确的。如果v等于A[j]那么这意味着我们已经找到了我们一直在搜索的元素。因此算法是正确的。

这些是正确的吗？

4

1 回答 1

2

这不是太糟糕，但你可以做一些改进。

循环不变式：“next after where...”语言很笨拙，并且您不会在算法正确的证明中使用它，因此没有理由维护它。像这样会更好：“在每次迭代开始时，不存在任何 i < j 使得 A[i] == v”。

维护：如果 A[j] != v 则循环继续。由于不存在任何 i < j 使得 A[i] == v 且 A[j]!=v，因此也不存在任何i <= j 使得 A[i] == v，并且循环不变量适用于 j 的下一个更大的值。

然后你可以在终止条件中使用它：如果循环在数组中找到 v 并返回它的索引，则循环提前终止。否则，循环不变量对于 j == length+1 成立，并且已知不存在任何 i <= length 使得 A[i]==v，即 v 不会出现在数组中。

于 2016-08-30T04:01:31.683 回答