验证偶数求和算法EvenSumming的循环不变式是否正确

原算法伪代码 #

EvenSumming(A)
outcome=0
for i=1 to n
 if A[i] is even
  outcome=outcome+A[i]
return outcome

用户提出的循环不变式及证明 #

循环不变式（LI）：每次迭代时，变量outcome始终为偶数，且最多由A[i....n]中的i-1个原始元素组成。
初始化：令i=1，outcome初始值为0，是偶数，且由A[1...n]中的0个元素组成。
维护：根据数学规则，两个偶数相加结果仍为偶数；每次迭代i递增1，第i次迭代前已遍历i-1个元素，故此时outcome是由A[i...n]中最多i-1个元素组成的偶数。
终止：终止时i>n即i=n+1，根据循环不变式，outcome仍为偶数，且最多由A[n]中的n个原始元素组成。

正确性判断及问题分析 #

你的循环不变式和证明存在多处问题，无法有效证明算法的正确性：

1. 范围描述错误：循环是从i=1到n依次处理A[1]到A[n]，迭代前的outcome是前i-1个元素（A[1..i-1]）的处理结果，而非A[i..n]中的元素，你搞反了数组范围。
2. 不变式偏离算法目标：循环不变式的核心作用是证明算法最终能得到预期结果，你的定义只强调了outcome是偶数、最多由若干元素组成，完全没关联到“累加所有偶数的和”这一算法核心目标，这样的不变式没有实际证明价值。
3. 维护步骤逻辑模糊：你只提到“两个偶数相加是偶数”，但没有明确迭代前后不变式的保持关系——即迭代前满足不变式，迭代后如何仍满足下一次迭代的不变式，这部分证明缺失关键逻辑。
4. 终止结论无效：终止时的结论只重复了“偶数、最多n个元素组成”，没有说明outcome就是数组中所有偶数的和，无法证明算法实现了预期功能。

正确的循环不变式及证明 #

循环不变式定义 #

在循环的第i次迭代开始前（即i取当前值准备执行循环体时），outcome等于数组A的前i-1个元素（A[1..i-1]）中所有偶数的和。

证明过程 #

• 初始化：当i=1时，前0个元素的和为0，outcome初始值为0，完全符合不变式。
• 维护：假设第k次迭代开始前，i=k，outcome是A[1..k-1]中所有偶数的和。迭代中处理A[k]：
  • 若A[k]是偶数，outcome += A[k]，此时outcome即为A[1..k]中所有偶数的和；
  • 若A[k]是奇数，outcome保持不变，仍然是A[1..k]中所有偶数的和。
    迭代结束后i=k+1，满足下一次迭代开始前的不变式。
• 终止：循环终止时i=n+1，根据不变式，outcome等于A[1..n]中所有偶数的和，这正是算法需要返回的结果，证明算法正确。

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