1

我了解到循环不变量应该在循环之前、循环体的开头、循环体的结尾和循环之后为真。如果条件没有副作用，这 4 分可以减少到 2 分：循环之前和循环体结束。这是Java中的一个示例，我在其中检查不变量assert：

private static int cube(int n) {
    int t = 1;
    int s = 0;
    int i = 0;

    assert (s == i*i*i && t == (i-1)*(i-1) && i <= n);

    while (i < n) {
        t = t + 2*i - 1;
        s = s + 3*t + 3*i + 1;
        i++;
        assert (s == i*i*i && t == (i-1)*(i-1) && i <= n);
    }

    return s;
}

我认为不变量表达式的冗余非常糟糕。如果 Java 允许我这样做，则断言可以减少到条件之前的一个断言点。

while ( i < n)
       ^

所以我想出了另一个概念解决方案，并将条件拆分为另一种方法：

private static int cubeElegant(int n){
    int t = 1;
    int s = 0;
    int i = 0;

    while (condition(n, t, s, i)){
        t = t + 2*i - 1;
        s = s + 3*t + 3*i + 1;
        i++;
    }

    return s;
}

private static boolean condition(int n, int t, int s, int i){
    assert (s == i*i*i && t == (i-1)*(i-1) && i <= n);
    return i < n;
}

我认为可读性很差，并且代码不必要地臃肿。我的解决方案是否可以在不使用第三方库的情况下通过合同不变检查以某种方式实现设计？Java中还有另一种更优雅的方式吗？

4

0 回答 0