如何证明算法的正确性？答案

【问题标题】：How can I prove algorithm correctness?如何证明算法的正确性？
【发布时间】：2019-01-24 18:01:47
【问题描述】：

我在Java中的这个练习有问题，我不明白如何在Java中证明这个sum方法

这是我做的：

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 + a[i] + a[i+1]
@DWuest：测试运行永远不是证明。
作为提示，考虑一下 P(n) 的 n 应该是多少。我建议它是数组的长度——在这种情况下，您的 P(0) 断言不成立，因为 a[0] 未定义（在 Java 中它是 IndexOutOfBoundsException）。然后对于 P(n+1)，您需要对循环在 P(n) 中的作用与在 P(n+1) 中的作用进行断言。在这两个循环中i 的可能值是多少？它们如何相互映射？

标签： java algorithm correctness

【解决方案1】：

循环不变量应该表示r 等于从索引0 到索引i 的a 的元素之和，排除在外。 IE。 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])

表示总和是增量获得的。

【讨论】：

【解决方案2】：

最简单的方法是定义一组输入及其预期输出。如果这是为了练习，您可能会得到这些值，或者您可能需要手动计算其中的一些值。然后我会使用这些已知输入编写单元测试，以查看每个输出是否与预期值匹配。如果您发现它们不匹配的地方，请仔细检查您的算法和的预期值。并排完成每个步骤并找出哪一个是错误的（或者两个都是错误的）。

另一种选择是用另一种语言编写相同的算法；理想情况下，您不能复制粘贴算法的实现以防止共享常见错误。然后使用 ton 的输入来运行两者。如果两种实现对每个输入都有匹配的结果，则您可以更有信心地确定两者都是正确的。

第三种选择是找到一组不变量，即在算法的不同阶段可证明为真的事物。然后在所有这些表明不变量成立的点上编写测试（或直接加入assert 语句）。诸如for every iteration of the "i" loop, r' >= r 之类的东西。然后针对大量输入运行它，如果这些断言中的任何一个失败，您就可以开始挖掘并找出您在算法中忘记处理的边缘情况（例如，如果输入为空怎么办？我如何处理否定数字？等等）

【讨论】：

测试不是证明手段。
使用 大量输入 运行是一种非常幼稚的方法。有两个原因：通常，算法在边界情况下而不是在域内失败。除非您专注于边界，否则大量输入是无用的；否则，吨数实际上相当于一箱。即便如此，只要有少量状态变量，通过任意测试发现错误的概率往往是无限小的。