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

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 在不变量中，所以我知道这不可能是正确的。我之前没有遇到过涉及布尔值的循环不变量并且很困惑，有人可以帮忙解释一下吗？

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

您可以在Dafny的在线版本中自动验证其正确性