用归纳法证明循环不变量成立

Question

//Precondition: n > 0
//Postcondition: returns the minimum number of decial digits
//               necessary to write out the number n
 int countDigits(int n){
1.    int d = 0;
2.    int val = n;
3.    while(val != 0){
4.        val = val / 10;     // In C++: 5 / 2 === 2
5.        d++;
6.    }
7.    return d;
}

不变量：就在评估第3行的循环保护之前，去掉最右边d位的n与val相同。(假设数字0需要0位才能写出，并且是唯一需要0位写出的数字(。

用归纳法证明循环不变量成立。

现在我一直认为，归纳法的证明是假设用k替换方程中的一个变量是真的，那么我必须证明k+1也是真的。但在这个问题上，我并没有真正得到一个等式，只是一块代码。这是我的基本情况：

就在评估第3行的循环保护之前，d等于0，在第2行，val==n，因此如果n去掉了最右边的0位，则为val。因此，基本情况成立。

我真的不知道如何写这之后的归纳步骤，因为我不知道如何证明k+1.

Answer 1

逻辑实际上与方程相同，只是用循环的n迭代替换方程中的k值：

1. 基本情况是循环不变量在开始循环之前保持不变
2. 你必须证明，如果不变量在迭代N之前成立，那么它在执行迭代N之后仍然成立

从1。和2。我们通过归纳得出结论，不变量在循环结束时成立(事实上，在任何迭代结束时(。

EDIT，这很有趣，因为循环以val == 0结束。您的不变量(在循环结束时仍然为true(是n，删除了最右边的d位数字，与val相同，因此删除了d位数字的n此时与0相同，因此d正确地是显示n所需的位数。