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

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

也许是这样，虽然这有点迂腐。

不变量：当 index = n 时，对于 n >= 1（在循环顶部检查条件），array[i] = i for 0

证明：证明是归纳法。在基本情况 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 for 0

证明：证明是归纳法。在基本情况 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 的值（在循环的顶部）。