loops - 简单 while 循环的循环不变量

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; } }

您可以通过在Dafny的在线版本中运行该程序来检查它是否确实进行了验证。