循环不变量应表示
我在Java中的这个练习有问题，我不明白如何在Java 中证明这个求和方法
这就是我做的：
P(0) : If r=0 and i=0 => r=0+a[0]
p(i+1) : r'= r + a[i] and i'=i+1
r'=r + a[i] + a[i+1]
public static int sum(int[] a) {
int r = 0;
int i = 0;
while (i < a.length) {
r = r + a[i];
i = i + 1;
}
return r;
}
r等于从索引0到索引i的a的元素之和，不包括在内。即r = Sum(k<i: a[k])。
然后我们可以注释
int r = 0;
int i = 0;
/* r = Sum(k<i: a[k]) */
while (i < a.length) {
r = r + a[i];
/* r = Sum(k<i: a[k]) + a[i] = Sum(k<i+1: a[k]) */
i = i + 1;
/* r = Sum(k<i: a[k]) */
}
/* r = Sum(k<=a.length: a[k]) */
证明的关键是
Sum(k<i: a[k]) + a[i] = Sum(k<i+1: a[k])
表示递增地获得总和。
最简单的方法是定义一组输入及其预期输出。如果这是一个练习，你可能会得到这些值，或者你可能需要手工计算一些。然后，我会使用这些已知的输入编写单元测试，看看每个输出是否与预期值匹配。如果你发现它们不匹配的地方，请仔细检查你的算法和的期望值。并排完成每个步骤，找出哪一个是错误的(或者如果两者都是错误的)。
另一种选择是用另一种语言编写相同的算法；理想情况下，不能复制粘贴算法的实现，以防止共享常见错误。然后使用吨的输入来运行两者。如果两个实现对每个输入都有匹配的结果，那么您可以对两者都是正确的有更高的信心。
第三种选择是找到一组不变量，即在算法的各个阶段可证明为真的东西。然后在所有显示不变量成立的点上编写测试(或者只放入assert语句)。像for every iteration of the "i" loop, r' >= r这样的东西。然后针对大量输入运行它，如果这些断言中的任何一个失败，你可以开始深入研究，找出你在算法中忘记处理的边缘情况(例如，如果输入为空怎么办？我如何处理负数？等等)