Loop инвариант простого, а петли

Question

Я видел пример программу, которая устанавливает все значения в массиве 0:

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

Он сказал, что часть инварианта цикла была 0<=i<n. Однако после завершения цикла цикл i будет равен n. Правильно ли я говорю, что это не является частью инварианта цикла? Если да, то в чем его следует заменить? Полный инвариант был For All j (0<= j < i --> a[i] = 0) & 0 <= i < n)

Answer 1

Инвариант цикла должен содержать запись цикла и сохраняться каждой итерацией, включая последнюю итерацию.

Поэтому инвариант цикла должен быть 0 <= i <= n

Чтобы поддержать мое требование, я предлагаю в качестве доказательства вашей программы, переведенной на автоматически проверяется язык 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; } }

Вы можете проверить, что эта программа действительно проверяет, запустив его в online version of Dafny.