循环边界与循环不变式 — 软件工程选择题
题目
某程序要在数组 a[0..n-1] 中求区间 [lo, hi)（0≤lo≤hi≤n）内元素之和。伪代码如下：
s←0; i←lo
while i < hi do
s←s+a[i]; i←i+1
end while
有人断言：每次进入循环体时，不变式「s = a[lo]+a[lo+1]+…+a[i-1]，且 lo≤i≤hi」成立，因而循环正常结束时 s 即为 a[lo..hi-1] 之和。关于该断言与边界，下列判断正确的是：
A. 断言正确；循环结束后有 i = hi-1，不变式给出正确和
B. 断言正确；初始化 i=lo、s=0 时不变式成立（空和），每轮保持，终止时 i=hi
C. 断言错误；不变式中应有 i<hi 而非 i≤hi，否则初始化不成立
D. 断言错误；正确不变式的上界应为 i≤n 而非 i≤hi