while-loop - 寻找循环不变量 - Hoare Triple

Question

从下面的代码中，我需要推断/选择一个循环不变量。

(|true|)
x = 0 ;
s = 0 ;
while ( x <= n ) {
    s = s + x ;
    x = x + 1 ;
}
(|s = n(n + 1)/2|)

给出的解决方案是

• s = (x-1)*x/2 ∧ (x ≤ n +1)

我不太明白它是如何达到上述解决方案的。

请帮助我了解如何从代码中得出这样的解决方案或其他循环不变量。

Answer 1

给定不变量，您可以轻松地检查它在循环之前、循环内和循环之后是否为真（是的，从 1 到 n 的整数相加得到 (n+1)*n/2 - 请参见三角形数）。由于它涵盖了循环中的所有相关变量（x和s），并且无法进一步细化（好吧，您可以添加^ x >= 0），因此它确实是不变量。

要自己推导，恐怕你需要事先了解三角数（或半平方）的公式。你当然可以写出s = sum of integers from 1 to x那部分，我认为它是一个有效的不变量。x <= n+1比较容易的部分。

外行寻找不变量的方法是尝试写出循环变量在其生命周期内在循环中所做的事情：

• s 总是保存直到 x 的整数之和
• x 遍历从 0 到 n 的整数，包括 0 到 n

然后用数学写出来。