我写了自己的琐碎的小函数（为了方便起见，php），希望有人能通过归纳法帮助构建一个证明，这样我就可以掌握它的基本技巧。
function add_numbers($max) {
//assume max >= 2
$index=1;
$array=array(0);
while ($index != $max) {
//invariant: ∀ k:1 .. index-1, array[k]=array[k-1]+1
$array[$index] = $array[$index-1]+1;
$index += 1;
}
}
结果是，每个索引处的值与索引本身相同，尽管这只是因为[0]被初始化为0。
我相信目标是（或应该是）证明不变量（它本身可能是可疑的，但希望能理解这一点）适用于k+1。
感谢
编辑：示例：http://homepages.ius.edu/rwisman/C455/html/notes/Chapter2/LoopInvariantProof.htm
也许是这样的，尽管这有点迂腐。
不变量：当index=n时，对于n>=1（在检查条件的循环顶部），array[i]=i表示0<=i<n.
证明：证明是通过归纳法。在基本情况n=1中，循环是第一次检查条件，主体尚未执行，并且我们有一个外部保证，即array[0]=0，来自代码早期。假设不变量适用于所有n到k。对于k+1，我们指定array[k]=array[k-1]+1。根据归纳假设，array[k-1]＝k-1，因此分配给array[k]的值是（k-1）+1=k。因此，不变量对于下一个，并且通过归纳每个n的值（在循环的顶部）都成立。
编辑：
function add_numbers($max) {
//assume max >= 2
$index=1;
$array=array(63);
while ($index != $max) {
//invariant: ∀ k:1 .. index-1, array[k]=array[k-1]+1
$array[$index] = $array[$index-1]+1;
$index += 1;
}
}
不变：当index=n时，对于n>=1（在检查条件的循环顶部），array[i]=i+63表示0<=i<n.
证明：证明是通过归纳法。在基本情况n=1中，循环是第一次检查条件，主体尚未执行，并且我们有一个外部保证，即array[0]=63，来自代码早期。假设不变量适用于所有n到k。对于k+1，我们指定array[k]=array[k-1]+1。根据归纳假设，array[k-1]=（k-1）+63=k+62，因此array[k]的赋值为（k+62）+1=k+63。因此，不变量适用于下一个，并且通过归纳每个，n的值（在循环的顶部）。