Что такое инвариант цикла данной программы?

Question

Я не знаю, как найти инвариант цикла. Я не уверен, с чего начать. Может кто-нибудь найти инвариант цикла данной программы и объяснить ваш метод, пожалуйста.

{n ≥ 0 ∧ i = 0}
while i < n − 1 loop
b[i] := a[i + 1];
i:=i + 1
end loop
{∀j.(0 ≤ j < n − 1 → b[j] = a[j + 1])}

Answer 1

1. while i < n − 1 loop
2. b[i] := a[i + 1];
3. i := i + 1
4. end loop

Инвариант: до шага 2, 1 <= i + 1 < n и для всех 0 <= j <= i - 1 является b[j] = a[j + 1],

Инвариант (тривиально) истинен, когда i = 0 (здесь нет j сытный 0 <= j <= i - 1). Более того, если это верно для некоторых i, это останется верным для i + 1, предоставлена i + 1 < n (иначе цикл закончен), потому что после 2 мы также знаем, что b[i] = a[i + 1],