二分查找

谓词通常用于使其他注释更清晰:

predicate sorted(a: array<int>)
   requires a != null
   reads a
{
   forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}
method BinarySearch(a: array<int>, value: int) returns (index: int)
   requires a != null && 0 <= a.Length && sorted(a)
   ensures 0 <= index ==> index < a.Length && a[index] == value
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != value
{
   // This one is a little harder. What should go here?
}
method BinarySearch(a: array<int>, key: int) returns (index: int)
   requires a != null && sorted(a)
   ensures ...
{
   ...
}

我们有和线性搜索一样的后置条件，因为目标是一样的。不同的是，现在我们知道数组是有序的。因为Dafny可以展开函数，所以在方法体中它也知道这一点。然后我们可以用这个性质来证明搜索的正确性。方法体如下所示:

predicate sorted(a: array<int>)
   requires a != null
   reads a
{
   forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}
method BinarySearch(a: array<int>, value: int) returns (index: int)
   requires a != null && 0 <= a.Length && sorted(a)
   ensures 0 <= index ==> index < a.Length && a[index] == value
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != value
{
   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] != value
   {
      var mid := (low + high) / 2;
      if a[mid] < value
      {
         low := mid + 1;
      }
      else if value < a[mid]
      {
         high := mid;
      }
      else
      {
         return mid;
      }
   }
   return -1;
}
   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] != value
   {
      var mid := (low + high) / 2;
      if a[mid] < value
      {
         low := mid + 1;
      }
      else if value < a[mid]
      {
         high := mid;
      }
      else
      {
         return mid;
      }
   }
   return -1;

这是一个相当标准的二分查找实现。首先，我们声明要搜索的范围。这可以被认为是钥匙可能存在的剩余空间。范围是包含-排他的，意味着它包括指数[low，high)。第一个不变量表示这个范围在数组内。第二个表示键不在这个范围之外的任何地方。在if链的前两个分支中，我们发现区间中间的元素不是键，因此我们移动区间以排除该元素及其相应一侧的所有其他元素。当移动范围的下端时，我们需要加上1，因为它在低端是包含的。如果不加1，那么当mid == low时，循环可能会永远继续下去，当low + 1 == high时就会发生这种情况。我们可以改变它，当low和high相差1时，循环退出，但这意味着我们需要在循环之后进行额外的检查，以确定是否在剩下的一个索引中找到键。在上面的公式中，这是不必要的，因为当low == high时，循环退出。但这意味着搜索范围内没有元素留下，因此没有找到键。这可以从循环不变量推导出来:

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

当low == high时，含义的第一部分的否定条件总是为真(因为没有i可以至少或严格小于相同的值)。因此，不变量表示数组中的所有元素都不是键，第二个后置条件成立。正如您所看到的，在这段代码中很容易出现一个错误。有了这些不变量，Dafny不仅可以证明代码是正确的，而且我们自己也可以更容易地理解代码的操作。

练习15.

点击查看题目及代码

修改BinarySearch函数体中的赋值，将low设置为mid，或将high设置为mid - 1。在每种情况下，哪里出了问题?

predicate sorted(a: array<int>)
   requires a != null
   reads a
{
   forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}
method BinarySearch(a: array<int>, value: int) returns (index: int)
   requires a != null && 0 <= a.Length && sorted(a)
   ensures 0 <= index ==> index < a.Length && a[index] == value
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != value
{
   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] != value
   {
      var mid := (low + high) / 2;
      if a[mid] < value
      {
         low := mid + 1;
      }
      else if value < a[mid]
      {
         high := mid;
      }
      else
      {
         return mid;
      }
   }
   return -1;
}
method BinarySearch(a: array<int>, value: int) returns (index: int)

#