以二进制搜索为例了解dafny代码终止

如何解决以二进制搜索为例了解dafny代码终止

有些事情我在这里不明白：

     0 <= i < a.Length && !(low <= i < high) ==> a[i] != key

在这一行中，我们为什么要！（low

为什么要设置low := mid + 1;？我知道这是因为循环可能不会终止（根据dafny告诉我的内容），但是有人可以给我一个例子吗？它在哪里发生以及如何发生？

predicate sorted(a: array<int>)
   reads a
{
   forall j,k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}

method BinarySearch(a: array<int>,key: int) returns (index: int)
   requires sorted(a)
   ensures 0 <= index ==> index < a.Length && a[index] == key
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
  
  var low,high := 0,a.Length;
   while low < high
      invariant 0 <= low <= high <= a.Length
      invariant forall i ::
         0 <= i < a.Length && !(low <= i < high) ==> a[i] != key
   {
      var mid := (low + high) / 2;
      if a[mid] < key
      {
         low := mid + 1;
      }
      else if key < a[mid]
      {
         high := mid;
      }
      else
      {
         return mid;
      }
   }
   return -1;
   
}

解决方法

1做什么

forall i :: (    (0 <= i < a.Length && !(low <= i < high))
             ==> a[i] != key )

是平均值吗？

这意味着key不在某些位置的数组a中发生。这些地方是0 <= i < a.Length为真但low <= i < high为假的地方。这是一张数组长度为12的图片，low为4，high为8。红色阴影部分为0 low <= i < high为假。因此，这个不变性就是说key不会在用红色和绿色阴影显示的任何位置中发生。换句话说，就是说如果键在数组中的任何位置，则它是红色的部分，而不是绿色的部分。

2为什么low := mid+1是a[mid] < key正确的任务？

首先，因为您知道a[mid]小于key，所以它不能等于key。此外，位置a[mid]左侧的每个位置的值都小于或等于a[mid]；因此这些位置的内容也不能等于key。因此，将所有这些位置涂成绿色是安全的。即将low设置为mid+1后，第二个不变式将保持为真。分配后，事情看起来像这样

您还必须考虑为什么第一个不变性仍然为真。您需要确保mid < high。您可以考虑为什么会这样。

因此，所有说明将low设置为mid+1都是安全的。即它不会使任何一个不变的假。如果您尝试将low := mid+1替换为low := mid+2以加快算法运行速度，将会发生什么？验证者将报告这是不安全的，因为它可能会使不变量之一变为假。

现在low := mid也将是安全的，但是问题在于，由于mid==low已经很正确，算法可能会在此时卡住。（当mid==low发生high==low+1情况。）因此low := mid+1达到了最佳效果。 2是不安全的。 0无法确保循环不断进展。