CLRS第4版2.1-2题SUM-ARRAY解法正确性验证请求

问题描述 #

请考虑如下SUM-ARRAY过程，它计算数组A[1:n]中n个元素的和。请为该过程给出一个循环不变式，并利用其初始化、保持和终止特性证明SUM-ARRAY过程返回A[1:n]中元素的和。

SUM-ARRAY(A, n)
1 sum = 0
2 for i = 1 to n
3     sum = sum + A[i]
4 return sum

我的解法（待确认） #

• 循环不变式：在每次循环迭代时，变量sum包含从A[0]到A[i-1]的累计和。
• 初始化：在第一次循环迭代前，当i=1时，A[i-1]=A[0]不包含任何元素，空元素的和为0。
• 保持：在每次循环迭代中，将A[i]的值加到sum变量中（第3行）。
• 终止：循环在i=n+1时终止，根据不变式，sum包含从A[0]到A[n]的所有元素的和。

解法修正与正确性验证 #

你的解法存在一处关键问题：题目明确数组是A[1:n]，不存在A[0]这个元素，因此循环不变式的范围描述有误，修正后如下：

正确循环不变式 #

在每次循环迭代（包括迭代前的初始状态）时，变量sum等于数组A[1]到A[i-1]的元素之和。

初始化验证

循环开始前（i=1），i-1=0，此时A[1]到A[0]是一个空区间，空区间的元素和为0，与sum的初始值0完全一致，满足循环不变式。

保持验证

假设在第k次迭代开始前（i=k），循环不变式成立：sum等于A[1]到A[k-1]的和。执行第3行代码后，sum更新为sum + A[k]，此时sum等于A[1]到A[k]的和。当迭代结束，i递增为k+1，此时sum正好等于A[1]到A[(k+1)-1]即A[1]到A[k]的和，循环不变式依然成立。

终止验证

循环在i=n+1时终止，此时根据循环不变式，sum等于A[1]到A[(n+1)-1]即A[1]到A[n]的元素之和，这正是题目要求计算的结果，因此过程返回的sum是正确的。

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