ループ不変条件ループ

Question

Iは0に、アレイ内のすべての値を設定するプログラム例を見ながら：

int a[n]; int i = 0; 
while(i < n) { 
    a[i] = 0; 
    i++; 
} 

これは、ループ不変の部分は0<=i<nだと言いました。しかし、ループが終了した後、私はnに等しくなります。これはループ不変の部分ではないと言って正しいのでしょうか？もしそうなら、それを何に置き換えるべきですか？ 完全不変量は

Answer 1

ループ不変式はループ入力を保持し、最後の反復を含むすべての反復によって保持されなければなりません。

したがって、ループ不変式が私の主張をサポートするために0 <= i <= n

する必要があり、私はあなたのプログラムが自動的に検証言語マイクロソフトDafnyに翻訳証拠として提供：

method Main(a:array<int>) requires a != null modifies a ensures forall j :: 0 <= j < a.Length ==> a[j] == 0 { var i:int := 0; while(i < a.Length) invariant 0 <= i <= a.Length invariant forall j :: (0 <= j < i ==> a[j] == 0) { a[i] := 0; i := i+1; } }

あなたは、このプログラムを確認することができます実際にはonline version of Dafnyで実行して確認します。