通过归纳证明算法的正确性

Question

我最近开始读一本关于数据结构的书，它从算法的介绍开始。在一个练习中，它要求通过归纳和循环不变量来证明算法。伪代码中的算法为：

Algorithm DEC2BIN(int n, int[] b)
Input: int n, array b
Output: b[i] contains the i-th bit of n's binary representation.
1: int x=n, k=0;
2:while(x>0){
3:   b[k]=x%2;
4:   x/=2;
5:   k++;
6:}
en of DEC2BIN

我说过：

设 P(n( 为语句 "b 包含 n 的二进制表示"。

当 n=1 时： 很明显，b=[1] 所以，P(1(。

设 P(N(。如何显示 P(n+1(？

Answer 1

首先提供一个适当的循环不变量。 例如

"运行后，循环 b 的k将包含n二进制表示的前k位数字"。

霍纳的方法和位置系统应该从上面的循环不变量开始证明陈述。