我写了自己的琐碎的小函数(为了方便起见,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的值(在循环的顶部)。