用于线性数组搜索的循环不变量

Question

int i = 0
boolean answer = false
while (i < a.length) {
    if a[i] == 0
        answer = true
    i = i + 1

其中“a”是一个整数数组。 我正在做一个问题文件，它问我这个循环不变量是什么，我已经确定代码可以计算出数组是否包含 0。但到目前为止我只能认为不变量是

i <= a.length

并且问题状态在不变量中包含变量 i、a 和答案，所以我知道这不可能。我以前没有遇到过涉及布尔值的循环不变量，我很困惑，谁能帮忙解释一下？

Answer 1

这是您在 Microsoft Dafny 中的循环实现，并指定了适当的循环不变量：

method Main(a:array<int>) returns (answer:bool)
   requires a != null
   ensures answer <==> (exists i :: 0 <= i < a.Length && a[i] == 0) 
{
   var i:int := 0;
   answer := false;
   while (i < a.Length)
     invariant 0 <= i <= a.Length;
     invariant !answer ==> !(exists j :: 0 <= j < i && a[j] == 0)
     invariant answer ==> (exists j :: 0 <= j < i && a[j] == 0)  
   {
     if a[i] == 0 {
        answer := true;
     }
     i := i + 1;
   }
}

您可以在online version of Dafny中自动验证其正确性