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という外部保証があります。kまでのすべてのnに対して不変量が成り立つと仮定します。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。

証明：証明は誘導によるものです。基本ケースn=1の場合、ループは初めて条件をチェックし、本体は実行されていません。また、コードの前半から、array [0]=63という外部保証があります。kまでのすべてのnに対して不変量が成り立つと仮定します。k + 1の場合、array [k] = array [k-1] + 1を割り当てます。帰納仮説から、array [k-1] =（k-1）+ 63 = k + 62であるため、値に割り当てられた配列[k]は（k + 62）+1 = k+63です。したがって、不変量は次の値を保持し、誘導によってnの値（ループの最上部）を保持します。

于 2012-02-26T23:28:37.950 に答える