loops - 给定程序的循环不变量是什么

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）时，不变量（通常）为真。此外，如果对于 some 为真，则对于,i将保持为真（否则循环结束），因为在 2 之后我们也知道.i + 1i + 1 < nb[i] = a[i + 1]