我不知道如何找到循环不变量。我不知道从哪里开始。任何人都可以找到给定程序的循环不变量并解释您的方法吗?
{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])}
-
while i < n − 1 loop
-
b[i] := a[i + 1];
-
i := i + 1
-
end loop
不变:在步骤 2 之前,b[j] = a[j + 1]
1 <= i + 1 < n
和所有0 <= j <= i - 1
。
当i = 0
时,不变性(平凡地(为真(没有满足0 <= j <= i - 1
j
(。此外,如果它对某些i
为真,则对于i + 1
将保持为真,前提是i + 1 < n
(否则循环完成(,因为在 2 之后我们也知道b[i] = a[i + 1]
。