CLRS切杆算法实现中4-6行循环的循环不变式及验证问询

循环不变式定义 #

针对代码中第4至6行的循环，循环不变式定义为：

当循环准备执行第i次迭代（i从1到n）时，变量q的值等于长度为n的钢杆仅考虑前i-1种切割方案（即第一段切割长度取1到i-1）时能获得的最大收益。若i=1（首次迭代前），因未考虑任何切割方案，q的初始值-inf代表“无有效方案的默认状态”。

初始化阶段证明 #

循环开始前，i=1，此时尚未执行任何迭代。根据循环不变式，需要q对应“前0种切割方案的最大收益”——也就是没有任何切割方式被评估，q被初始化为-inf，完全符合这一要求，因此初始化时循环不变式成立。

保持阶段证明 #

假设在第i次迭代开始前，循环不变式成立：即q存储了第一段长度取1到i-1时的最大收益。

在本次迭代中，计算p[i] + cut_rod(p, n-i)——这是第一段切割长度为i时的总收益。随后将q更新为当前q与该值的最大值，此时q就代表了第一段长度取1到i时的最大收益，恰好满足第i+1次迭代开始前的循环不变式要求（此时对应前i种切割方案）。因此，每次迭代后循环不变式仍保持成立。

终止阶段证明 #

循环终止时，i = n+1（循环遍历完1到n的所有值）。根据循环不变式，此时q存储了第一段长度取1到n时的最大收益——这覆盖了长度为n的钢杆的所有可能切割方案：

• 若选择切割，第一段长度可从1到n-1，剩余部分递归求解；
• 若选择不切割，对应第一段长度为n，收益为p[n] + cut_rod(p, 0) = p[n]，已被纳入计算。

因此，终止时q的值就是长度为n的钢杆能获得的最大收益，与函数返回值一致，验证了算法的正确性。

内容的提问来源于stack exchange，提问作者Rajesh Kumar