Schleifeninvariante einfache while-Schleife

Question

I ein Beispielprogramm sah den auf 0 jeden Wert in einem Array setzt:

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

Es wird gesagt, dass ein Teil der Schleife invariant 0<=i<n ist. Nachdem die Schleife beendet ist, wird jedoch gleich n sein. Korrigiere ich, dass dies nicht Teil der Schleifeninvariante ist? Wenn ja, mit was soll es ersetzt werden? Die vollständige Invariante war For All j (0<= j < i --> a[i] = 0) & 0 <= i < n)

Answer 1

Die Schleifeninvariante muss Schleife beibehalten und wird von jeder Iteration einschließlich der letzten Iteration beibehalten.

Deshalb ist die Schleifeninvariante 0 <= i <= n sein sollte

meinen Anspruch zu unterstützen, biete ich als Beweis Ihr Programm übersetzt in die automatisch überprüft Sprache Microsoft 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; } }

Sie, dass dieses Programm überprüfen in der Tat verifiziert, indem es in der online version of Dafny läuft.