这是在数组中进行线性搜索的伪代码,如果在数组中找到了所需的元素,则返回索引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] != e
for allj < i
。
初始化:在第一个循环迭代之前,由于数组是空的,所以不变量保持不变。
维护:循环不变量在每次迭代中都会被维护,因为在第次迭代中会有一些这样的循环然而,在这种情况下,对于循环的第i
-次迭代,返回值j < i
,并且没有循环的第A[j] == e
-次迭代,这是一个矛盾。
终止当循环终止时,可能有两种情况:一种是它在j
迭代之后终止,并返回j
,在这种情况下,i
条件确保i <= A.length
另一种情况是i
超过if
,在这种情况下,通过循环不变量,我们得到对于所有A[i] == e
,i
,返回NIL是正确的。