蛮力法最大子数组算法正确性证明：循环不变式设计困境

我完全懂你的困扰——蛮力法最大子数组里的全局max_sum变量确实会给循环不变式的设计添乱，因为它会被内层循环持续修改，打破单纯的局部状态描述。咱们一步步拆解来解决这个问题。

先明确蛮力法的伪代码 #

首先，先把典型的蛮力法最大子数组算法写出来，方便后续讨论：

max_sum = -∞
n = length(arr)
for i from 0 to n-1:
    current_sum = 0
    for j from i to n-1:
        current_sum += arr[j]
        if current_sum > max_sum:
            max_sum = current_sum
return max_sum

分层次设计循环不变式 #

这里要把外层循环和内层循环的不变式分开设计，同时把全局的max_sum状态纳入每个层次的描述中。

外层循环的循环不变式 #

在每次外层循环迭代开始前（即i取当前值时），max_sum存储的是所有起点小于i的子数组中的最大子数组和。

内层循环的循环不变式 #

在每次内层循环迭代开始前（即j取当前值时）：

1. current_sum存储的是子数组arr[i..j-1]的和（当j=i时，current_sum为0，对应空数组的和）；
2. max_sum存储的是所有起点小于i的子数组，以及所有起点等于i且终点小于j的子数组中的最大子数组和。

验证循环不变式的正确性 #

循环不变式需要满足三个核心条件：初始化、保持、终止。

1. 初始化 #

• 外层循环初始化：外层循环开始前，i=0，此时不存在起点小于0的子数组，max_sum初始化为-∞，完全符合外层循环的不变式；
• 内层循环初始化：每次内层循环开始前，j=i，current_sum=0（对应空数组arr[i..i-1]的和），max_sum保持外层循环迭代开始时的值（即所有起点小于i的子数组的最大值），此时不存在起点等于i且终点小于j的子数组，因此内层循环的不变式成立。

2. 保持 #

• 内层循环保持：执行内层循环体时，首先将arr[j]加到current_sum中，此时current_sum变为arr[i..j]的和；接着比较current_sum与max_sum，若前者更大则更新max_sum。这一步完成后，max_sum就包含了所有起点小于i的子数组，以及所有起点等于i且终点≤j的子数组的最大值，恰好满足下一次内层循环迭代（j递增1）的不变式要求；
• 外层循环保持：当内层循环终止时，j=n，此时max_sum已经包含了所有起点等于i的子数组的最大值。外层循环将i递增1后，max_sum自然对应所有起点小于i+1的子数组的最大值，符合外层循环下一次迭代的不变式。

3. 终止 #

当外层循环终止时，i=n，此时max_sum存储的是所有起点小于n的子数组的最大值——也就是整个数组中所有可能的子数组的最大值（因为所有子数组的起点范围都是0到n-1）。因此算法返回的max_sum就是正确的最大子数组和。

关键思路总结 #

你之前的困惑核心在于没有把全局的max_sum的范围限定纳入内层循环的不变式中。不要把max_sum当成“全局最大值”，而是要明确它在每个迭代步骤中代表的是截至当前处理过的所有子数组的最大值，这样就能把它和current_sum的局部状态结合起来，设计出严谨的循环不变式。

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