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

【问题标题】：Is this a correct invariant for this loop?这是这个循环的正确不变量吗？
【发布时间】：2016-03-03 16:59:48
【问题描述】：

这是在数组中进行线性搜索的伪代码，如果在数组 A 中找到所需的元素 e，则返回索引 i，否则返回 NIL（来自 CLRS book，第 3 版，练习2.1-3）：

LINEAR_SEARCH (A, e)
    for i = 1 to A.length
        if A[i] == e
            return i
    return NIL

我试图从中推断出一个不变量的循环，所以根据我的理解，我认为它的代表是这样一个事实，即在循环中的任何给定时刻，子数组 A[1..i-1] 只包含相等性测试被证明是错误的。

具体来说，在第一次迭代之前i-1 == 0 这意味着子数组的长度为空，因此不能有一个元素v 属于它，这样v == e。在任何下一次迭代之前，作为等式测试也是退出条件，假定的不变属性必须仍然成立，否则循环将已经结束。在终止时，要么函数即将返回一个索引（在这种情况下，循环不变量是微不足道的），要么返回 NIL（在这种情况下i == A.length + 1，所以循环不变量对任何 @987654331 都成立@)。

上面说的对吗？如果不是，您能否提供一个正确的循环不变量？

感谢您的关注。

【问题讨论】：

标签： algorithm loops clrs loop-invariant

【解决方案1】：

循环不变量：在 for 循环的每次迭代开始时，我们将 A[j] != e 用于所有 j < i。
初始化：在第一次循环迭代之前，由于数组为空，因此不变量成立。
维护：循环不变量在每次迭代中都得到维护，否则在i-th 迭代中会有一些j < i 使得A[j] == e。但是，在这种情况下，对于循环的第 j-th 次迭代，返回值 j，并且没有 i-th 循环的迭代，这是矛盾的。
终止当循环终止时，可能有两种情况：一种是在i <= A.length迭代后终止，并返回i，此时if有条件确保A[i] == e。另一种情况是i超过A.length，在这种情况下，通过循环不变量，对于所有j <= A.length、A[j] != e，这个返回的NIL是正确的。

【讨论】：