循环不变式的性质

发布网友发布时间：2022-10-01 09:49

共1个回答

热心网友时间：2024-08-23 19:37

一般而言,用这个式子表示希望得到的结果,如果在循环的每一步,这个式子都是正确的,那么循环结束后,这个式子也正确,并得到了期望的结果.
lenovo所引用的文章里的例子是这样的:
QUOTE:
apvector<int> list(n); // n is some positive integer
int k, indexMax;
<code which assigns values to all entries in list>
indexMax = 0;
for(k = 1; k < list.length(); k++){
// invariant true here
if (list[k] > list[indexMax])
indexMax = k;
}
这是一个很简单的求最大值(在数组中的下标)的问题,在循环内// invariant true here 处可以指明始终成立的不变式为:
QUOTE:
在当前的k之前, 最大值的下标是indexMax, 而且0<=indexMax<k
可以看出这个式子在整个循环过程中是始终成立的,所以在循环结束的时候(k=list.length()),这个式子也成立,
即:
QUOTE:
在整个list中,最大值的下标是indexMax, 而且0<=indexMax<list.length()
这就是我们期望得到的结果,也就是说我们得到了最大值的下标
根据循环不变式的3个特性，再结合归纳法，证明我们写的循环是正确滴。
一句话：,如果在循环的每一步,这个式子都是正确的,那么循环结束后,这个式子也正确
算法导论中的循环不变性(loop invariant)：
初始化：在循环的第一轮迭代前是正确的；
保持：如果在循环的某一次迭代开始之前是正确的，那么在下一次迭代开始之前，也是正确的；
终止：当循环结束，不变式给了我们一个有用的性质。
当头两个性质成立时，就能保证循环不变式在循环的每一轮迭代开始之前，都是正确的，有关循环不变式的第三项可能是最重要的，因为我们是用不变式来证明算法的正确性。