java - 解释循环不变量

Question

这是过去试卷中的一道题。

为什么循环不变量说i<=n当循环测试显示 i<n .

是一个合适的答案:它说 i<=n作为i将等于 n关于 while 循环的失败条件。因此 i 的第 6 次迭代将等于 n失败条件下的值 6。但是，while 循环本身声明 i<n作为i从 0 开始，将完成一次循环 i等于 5。

private int n =6;

public int fact(){
    int i = 0;
    int f = 1;

    /**loop invariant
     * 0<=i<=n
     * f=i!
     */
    while(i<n){//loop test
        i=i+1;
        f=f*i;
    }

    return f;
}

Answer 1

因为 Post-Condition是i==n当循环离开时。 Pre-Condition进入循环时是i==0 .循环内部 i正在向 n 计数.所以不变量是0 <= i <= n .

我省略了 f 的不变部分在我的解释中。这实际上还不够，因为不变量必须捕获循环的正确性和含义。

private int n = 6;

public int fact(){
    int i = 0;
    int f = 1;

    /* loop invariant: 0 <= i <= n && f == i! */
    /* PRE: i == 0 && f == i! */
    while (i < n) {
        i = i + 1;
        f = f * i;
    }
    /* POST: i == n && f == i! */

    return f;
}