这个循环不变量是否正确？答案

【问题标题】：Is this loop invariant correct?这个循环不变量是否正确？
【发布时间】：2016-08-30 01:41:57
【问题描述】：

线性搜索循环的伪代码：

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] 那么这意味着我们找到了我们一直在搜索的元素。因此算法是正确的。

这些是正确的吗？

【问题讨论】：

标签： algorithm loop-invariant

【解决方案1】：

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

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

维护：如果 A[j] != v 则循环继续。由于不存在任何 i

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

【讨论】：