用归纳法证明循环不变式保持
用归纳法证明循环不变式保持
提问于 2014-04-24 23:18:25
//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行的循环保护之前，n的最右边d位数被移除，这与val是完全相同的。(假设，数字0取0位数写出，是唯一取0位数写出的数字)。
用归纳法证明循环不变式有效。
现在我一直认为用归纳法证明，假设用k替换方程中的变量是真的，那么我必须证明k+1也是真的。但在这个问题上，我并没有得到一个等式，只是一个代码块。这是我的基本案例：
在计算第3行上的循环保护之前，d等于0，在第2行上，val == n，所以如果n的最右边0位数被移除，它就是val。因此，基本大小写成立。
在此之后，我不太确定如何编写归纳步骤，因为我不知道如何证明k+1。
回答 1
Stack Overflow用户
发布于 2014-04-24 23:40:24
逻辑实际上与方程相同，只是用循环的k迭代替换了方程中的n值：
- 基本情况是，循环不变量在开始循环之前保持不变；
- 您必须证明，如果不变量在迭代
N之前保持不变，那么它在迭代N执行之后仍然有效。
从1.和2.我们通过归纳法得出结论，不变量在循环结束时(实际上是在任何迭代结束时)保持不变。
编辑，这很有趣，因为循环以val == 0结尾。您的不变量(在循环结束时仍然为真)为n，其最右边的d位与val相同，因此删除d数字的d在此时与0相同，因此d正确地表示显示n所需的数字数。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/23281558
复制相关文章
相似问题
腾讯云开发者
