从下面的代码中，我需要推断/选择一个循环不变量。
(|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(
我不太明白它是如何达到上述解决方案的。
请帮助我如何从代码中派生出这样的解决方案或其他循环不变量。
给定不变量，您可以轻松地在循环之前、内部和之后检查它是否为真(是的，将 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 的整数，包括
然后用数学写出来。