通过循环不变式（归纳法）证明正确性

Question

我编写了自己的简单小函数（为了方便起见，使用 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;
  }
}

结果是每个索引处的值与索引本身相同，尽管只是因为 a[0] 被初始化为 0。

我相信目标是（或应该是）证明不变式（这本身可能是可疑的） ，但希望能明白这一点）对于 k+1 成立。

谢谢

编辑：示例： http://homepages.ius.edu/ rwisman/C455/html/notes/Chapter2/LoopInvariantProof.htm

Answer 1

也许是这样的，尽管这有点迂腐。

不变：当索引 = n 时，对于 n >= 1（在循环顶部检查条件），array[i] = i 对于 0 <= i <名词

证明：证明是通过归纳法。在基本情况 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;
  }
}

不变：当索引 = n 时，对于 n >= 1 （在检查条件的循环顶部）， array[i] = i + 63 for 0 <= i < <名词

证明：证明是通过归纳法。在基本情况 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 的下一个值，并且通过归纳，每个值都成立（在循环的顶部）。