循环与不变量

循环不变量把重复执行变成可以检查的证明。扫描最大值时，每次来到循环头都保持：best 等于已处理前缀 values[0:i] 的最大值。初始化建立条件，每轮恢复条件，退出时再用它推出最终答案。

不变量绑定到明确的检查点。本课的检查点在 Python 判断 i < len(values) 之前。循环体中可以暂时使用扩展到下一个元素的形式，但回到检查点前必须恢复原形式。

二分查找、双指针或复杂的 while 容易写错边界时，可以先说明已处理区域保证什么。第一个不满足条件的检查点，能帮助定位错误。

循环不变量如何工作

证明有三步：

1. 初始化：第一次检查条件前，不变量成立。
2. 保持：假设一轮开始时成立，证明执行一轮后仍成立。
3. 终止：结合不变量和为假的循环条件，推出结果。

最大值扫描的不变量是 best = max(values[0:i])。切片不含 i，恰好覆盖已处理元素。设 best = values[0]、i = 1，初始前缀为 [values[0]]，其最大值就是 values[0]。

一轮中，未处理候选是 values[i]。best = max(best, values[i]) 建立 best = max(values[0:i + 1])；再执行 i = i + 1，同一个边界换成新 i，恢复循环头形式 best = max(values[0:i])。

逐步演示

默认使用 values = [3, 1, 4, 2, 5]。

1. 第 1 行设 best = 3，第 2 行设 i = 1。前缀为 [3]，首次检查前不变量成立。
2. 1 < 5 为真。候选 values[1] = 1，max(3, 1) 保持 best = 3。i 增到 2，对前缀 [3, 1] 恢复不变量。
3. 2 < 5 为真。候选是 4，best 改为 4。i = 3 时，前缀 [3, 1, 4] 的最大值为 4。
4. 3 < 5 为真。候选是 2，best 保持 4。i 增到 4，已证明的前缀延伸到索引 3。
5. 4 < 5 为真。候选是 5，best 改为 5。i 增到 5，前缀覆盖整个列表。
6. 5 < 5 为假，循环停止，第 6 行打印 5。
7. 只把第 1 行改成 best = 0，再使用 [-8, -3, -11, -2, -5]。第一个检查点就有 0 ≠ max([-8]) = -8，初始化没能建立证明。
8. 所有候选都为负数，best 始终为 0，程序输出 0，但真正最大值是 -2。

移动括号表示循环头的证明边界。在检查和更新时，即使 best 已考虑候选，候选仍暂时位于括号外。只有推进 i 后，括号移动，循环头公式才恢复。

错误初始化如何破坏证明

全负数列表中，best = 0 引入了输入之外、比所有候选都大的值。第一次循环头的不变量已经为假，后续更新始终保留 0，最后输出了列表里没有的值。

终止如何完成证明

退出时，i < len(values) 为假。i 每次只增加一，不越过长度，因此此时 i = len(values)。代入不变量：

best = max(values[0:i]) = max(values[0:len(values)])。

第二个切片覆盖整个列表。初始化和保持已经证明 best 的含义，退出条件让前缀覆盖全部输入，程序因此可以输出它。

时间与空间复杂度

非空列表长度为 n 时，先用第一个值初始化，再检查 n - 1 个候选。每轮是常数工作，时间为 O(n)。只保存 best、i 和临时候选，额外空间为 O(1)。

边界情况

• 单元素。 初始化已覆盖整个列表，第一次条件即为假，循环体零次执行，输出唯一元素。
• 空列表。 values[0] 抛出 IndexError。此实现要求至少一个元素，空输入实验直接展示这个前提，不用哨兵掩盖。
• 全负数。 从首元素初始化仍正确，从 0 初始化会出错。
• 最大值重复。 不变量讨论最大值本身，再次遇到相同最大值无需修改 best。
• 最大值在末尾。 最后一轮仍要恢复不变量，随后才进行为假的条件检查。

常见错误

• 声称每条语句之后不变量都成立。更新期间使用的是 i + 1 形式，递增后才恢复循环头形式。
• 未证明输入条件就选择 best = 0。方便的哨兵可能改变问题；本课的前缀最大值不变量还要求初始化与第一个前缀相符。
• 读取 values[i] 前先增加 i。这会跳过候选，也可能越界。
• 只证明初始化和保持，不证明终止。只有退出状态让前缀覆盖整个输入，不变量才能给出后置条件。
• 把几个正确输出当成证明。测试可以找到反例，三项证明义务才覆盖所有满足前提的输入。

本课的简化

动画一次高亮一条 Python 语句。第 4 行占两拍：先求 max(best, values[i])，再写入 best。解释器内部更细的操作、对象、栈帧和异常处理不在画面中。证明假定输入是有限、非空、元素可比较的序列，使用普通整数索引，不模拟并发修改或自定义比较行为。