algorithm - 这个循环不变量是否正确？

Question

线性搜索循环的伪代码:

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

我写的循环不变量:

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

初始化:

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

维护:

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

终止:

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

这些正确吗？

Answer 1

还不错，但您可以做一些改进。

循环不变量:“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 不出现在数组中。