ループインバリアント（誘導）による正しさの証明

Question

私は自分の小さな関数（php for convenience）を書いていましたが、誰かがそれを誘導する証明を構築するのを助けてくれることを望んでいました。

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

Answer 1

何か、多分、これは少し知識をひけらかすですが。

不変式：n> = 1の場合（条件を確認するループの最上部）、配列[i] = iが0の場合< = i <の場合。

証明：証明は誘導によるものです。 n = 1の基底の場合、ループは最初に条件をチェックしており、ボディは実行されておらず、コードの前の方から配列[0] = 0を保証しています。不変量がkまでのすべてのnに対して成立すると仮定してください。帰納仮説から、配列[k-1] = k-1であるので、配列[k]を割り当てられた値は（k-1）であるので、配列[k] = array [k- ）+1 = k。したがって、不変量は、次のものと、帰納法によって、nの値（ループの最上部）を保持します。

EDIT：

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（それは条件をチェックし、ループの先頭に）、アレイは[I] = iは0 < 63を+ = i < n。

証明：証明は誘導によるものです。 n = 1の基底の場合、ループは最初に条件をチェックしており、ボディは実行されておらず、コードの前の方からarray [0] = 63という外側の保証があります。不変量がkまでのすべてのnに対して成立すると仮定してください。帰納仮説から、配列[k-1] =（k-1）+ 63 = k + 62であるので、配列[k] = array [k-1] [k]は（k + 62）+1 = k + 63である。したがって、不変量は、次のものと、帰納法によって、nの値（ループの最上部）を保持します。