这是在数组中进行线性搜索的伪代码,如果在数组中找到了所需的元素,则返回索引i,否则返回e(这是CLRS手册第3版,练习2.1-3):

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

我试图从中推断出一个循环不变量,所以根据我的理解,我认为一个是由这样一个事实表示的:在循环中的任何给定时刻,子数组A只包含等式测试证明为假的值。
具体来说,在第一次迭代NIL之前,这意味着子数组的长度为空,因此不能有属于它的元素A[1..i-1],这样i-1 == 0在任何下一次迭代中,作为相等性测试也是一个退出条件,假设不变的属性必须保持真,否则循环就已经结束了。在终止时,要么函数将返回一个索引(在这种情况下,循环不变量非常正确),要么返回NIL(在这种情况下v,因此循环不变量对于任何v == e
以上是否正确?请您提供一个正确的循环不变量,以防它不是?
谢谢你的关注。

最佳答案

循环不变量:在for循环的每次迭代开始时,我们都有A[j] != efor allj < i
初始化:在第一个循环迭代之前,由于数组是空的,所以不变量保持不变。
维护:循环不变量在每次迭代中都会被维护,因为在第次迭代中会有一些这样的循环然而,在这种情况下,对于循环的第i-次迭代,返回值j < i,并且没有循环的第A[j] == e-次迭代,这是一个矛盾。
终止当循环终止时,可能有两种情况:一种是它在j迭代之后终止,并返回j,在这种情况下,i条件确保i <= A.length另一种情况是i超过if,在这种情况下,通过循环不变量,我们得到对于所有A[i] == ei,返回NIL是正确的。

08-25 09:13
查看更多