1

我编写了自己的琐碎小函数（为方便起见是 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

4

1 回答 1

1

可能是这样的，尽管这有点迂腐。

不变量：当 index = n 时，对于 n >= 1（在循环顶部检查条件），array[i] = i for 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 for 0 <= i < n。

Proof: The proof is by induction. In the base case n = 1, the loop is checking the condition for the first time, the body has not executed, and we have an outside guarantee that array[0] = 63, from earlier in the code. Assume the invariant holds for all n up to k. For k + 1, we assign array[k] = array[k-1] + 1. From the induction hypothesis, array[k-1] = (k-1) + 63 = k + 62, so the value assigned array[k] is (k+62)+1 = k+63. Thus the invariant holds for the next, and by induction every, value of n (at the top of the loop).

于 2012-02-26T23:28:37.950 回答