数组最大值查找函数的部分正确性证明：循环不变量维护解析

先唠清楚这个Eiffel函数是干啥的：它从非空数组里揪出最大值，核心逻辑靠循环实现，教授说的“部分正确性”，其实就是要证明两件事——循环结束时结果一定是对的，而且循环不会无限运行（咱们今天重点拆解不变量维护的部分）。

先搞明白循环不变量到底说啥 #

函数里的不变量有两种写法，本质是同一个意思：

• 数学表达式：∀j | a.lower ≤ j < i • Result ≥ a[j]
• Eiffel代码版：across a.lower |..| (i − 1) as j all Result >= a [j.item]

翻译成大白话就是：不管循环走到哪一步，在检查终止条件之前，当前的Result一定是数组从第一个元素（a.lower）到第i-1个元素这个范围内的最大值。简单说就是：我们已经扫过的元素里，没有比Result更大的。

一步步证明不变量是怎么被维护的 #

要证明部分正确性，得走三个关键环节：初始化时不变量成立，每次循环都能保住这个不变量，循环结束时不变量能导出正确结果。咱们挨个说：

1. 刚开始的时候，不变量成立吗？ #

循环启动前的from块是这么写的：

i := a.lower
Result := a [i]

这时候i等于数组的第一个元素下标，那i-1就比第一个下标还小，对应的范围a.lower |..| (i-1)是个空区间——连一个元素都没有。对于空集合来说，“所有元素都满足Result≥a[j]”这句话是天然成立的（毕竟没元素要验证），所以不变量一开始就站稳了脚跟。而且这时候Result就是第一个元素，也符合“已检查的元素（就它自己）的最大值就是它”的逻辑，没毛病。

2. 每次循环跑一圈，不变量还能保住吗？ #

假设在某次循环开始前，不变量是成立的——也就是Result已经是a.lower到i-1的最大值。接下来执行循环体（标准的find_max循环体应该是：i := i + 1; if a[i] > Result then Result := a[i] end）。

咱们分两种情况看：

• 如果a[i] ≤ Result：这时候不用更新Result，它还是原来的数值。原来的Result已经是前i-1个元素的最大值，现在加上a[i]，它也没超过Result，所以Result依然是前i个元素的最大值，不变量继续成立。
• 如果a[i] > Result：这时候把Result换成a[i]。原来的Result是前i-1个元素的最大值，现在a[i]比它还大，那新的Result自然就是前i个元素的最大值，不变量照样成立。

不管哪种情况，跑完循环体后，不变量都能稳稳保持，这就证明了每次迭代都能维护住这个“承诺”。

3. 循环结束时，不变量能帮我们得到正确结果吗？ #

循环的终止条件是i > a.upper。当循环停下来的时候，不变量依然成立：Result是a.lower到i-1的最大值。这时候i已经超过了数组的最后一个下标，那i-1刚好就是数组的最后一个下标a.upper——也就是说，Result是整个数组所有元素的最大值，完全符合函数要返回的结果！这就把“部分正确性”给坐实了。

最后总结下 #

循环不变量就像我们给自己定的一个“规矩”：每次循环前，都确保已经检查过的元素里，Result是最大的。从一开始的初始状态，这个规矩一直守得住，直到循环结束时，我们已经检查完了所有元素，这个规矩就变成了“Result是整个数组的最大值”，完美达成目标。

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