怎样找"循环不变式"?

[syncher]

算法导论中讲到一个概念就是循环不变式,知乎上有人提出"如何正确理解循环不变式?"(参见:https://www.zhihu.com/question/26700198) ,我现在大致理解了一些,大概就是每次执行循环总有一些特性保持不变,但是对于一个具体的案例还是不会找循环不变式,如求一个数组的最大值:

max = A[1] for i = 1 to A.length if A[i] > max max = A[i]

请问该如何找该算法中的循环不变式?

[yangff]

max 是 a[1..i]的最大值

[yangff]

是这样的，现在我要证明`max = A[1] for i = 1 to A.length if A[i] > max max = A[i]`这个程序能给出 A[]这个数组的最大值，我们没办法一条一条地考察这个程序，因为循环的存在，他可能被执行任意多次

怎么做，一个直观的想法就是，我要有一个特性能得到最后的正确性，并且这个特性总成立。

在这里就是

“对于一个有限长度的 n （循环终止时）， max 是 A[1..n]中最大的”

那么对于这段程序，用归纳法，显然 n=1 的正确性

若假设 n=k 正确，当 n=k+1 时，我们首先有 max 是 a[1..k]的最大值，又由` A[i] > max max = A[i] `, 使之成为 A[1..k+1]的最大值

于是就可归纳得到对于任意长度（终止的 n ） max ，也就是 max 是 A[1..n]中最大的得证

从而证明了循环的正确性

[syncher]

感谢楼主,好像懂了,比如:
for i = 1 to n sum += i 这个循环体只有一个表达是 sum += i; 那么循环中保持不变的特性就是 sum 总是 1,2,...,i 的和,这个特性就是循环不变式,是吗?

[syncher]

@yangff 感谢楼主,好像懂了,比如:
for i = 1 to n sum += i 这个循环体只有一个表达是 sum += i; 那么循环中保持不变的特性就是 sum 总是 1,2,...,i 的和,这个特性就是循环不变式,是吗?

[yangff]

@syncher 嗯