0

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

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，所以循环不变量对任何1 < j < i）。

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

感谢您的关注。

4

1 回答 1

1

  • 循环不变量：在 for 循环的每次迭代开始时，我们都有A[j] != efor all j < i。

  • 初始化：在第一次循环迭代之前，不变量成立，因为数组是空的。

  • 维护：在每次迭代中都维护循环不变量，因为否则在i第 - 次迭代中会有一些j < i这样的A[j] == e。但是，在这种情况下，对于j循环的第 - 次迭代，j返回值，并且没有i循环的第 - 次迭代，这是矛盾的。

  • 终止当循环终止时，可能有两种情况：一种是在i <= A.length迭代后终止，并返回i，在这种情况下，if条件保证了A[i] == e。另一种情况是i超过A.length，在这种情况下，通过循环不变量，对于所有j <= A.length, A[j] != e，这个返回的 NIL 是正确的。

于 2016-03-03T18:35:59.620 回答