判断给定循环不变式是否适用于有序数组两数之和验证代码

1. 原命题是否为合适的循环不变式？ #

不是。原因很直接：

• 循环不变式的核心要求是在循环启动前、每次迭代结束后都必须恒成立。
• 你提出的命题“子数组arr[left:right+1]中存在和为k的数对”默认了数对一定存在，但如果原数组本身就没有符合条件的数对，那么初始状态（left=0，right=len(arr)-1，即整个数组）下这个命题就是假的，直接违背了循环不变式的前提。
• 后续迭代中，这个命题也无法保证持续成立——比如原数组无符合条件的数对时，所有迭代阶段的子数组都不存在数对，命题始终为假，根本起不到“不变式”的验证作用。

2. 什么样的循环不变式才是最优选择？ #

最优的循环不变式必须覆盖数对存在和不存在两种场景，确保在整个迭代过程中始终成立，从而完整证明代码的正确性：

循环不变式：原数组中存在和为k的数对，当且仅当子数组arr[left:right+1]中存在这样的数对。

为什么这个不变式有效？ #

• 初始状态：left=0，right=len(arr)-1，子数组就是整个原数组，“原数组存在数对等价于子数组存在数对”显然成立。
• 迭代过程：
  • 若current_sum = arr[left] + arr[right] < k：因为数组有序，arr[left]是当前子数组最小元素，它和最大元素arr[right]的和都小于k，说明arr[left]和子数组中任何其他元素的和都会小于k，因此可以安全右移left（排除arr[left]）。此时原数组存在数对等价于新子数组（arr[left+1:right+1]）存在数对，不变式保持成立。
  • 若current_sum > k：同理，arr[right]是当前子数组最大元素，它和最小元素arr[left]的和都大于k，说明arr[right]和子数组中任何其他元素的和都会大于k，因此可以安全左移right（排除arr[right]），不变式同样成立。
  • 若current_sum == k：直接返回True，符合预期。
• 循环结束：当left >= right时，子数组最多只有一个元素，不可能存在数对。根据不变式，原数组也不存在这样的数对，返回False完全正确。

总结 #

你提出的命题不能作为合适的循环不变式，因为它只考虑了数对存在的情况，忽略了不存在的场景，不满足循环不变式的基本要求。而“原数组存在和为k的数对当且仅当当前子数组存在该数对”的双向等价命题，才是能完整证明代码正确性的最优选择。

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