量词

Dafny中的量词通常采用forall表达式的形式，也称为通用量词。顾名思义，如果某个属性对某个集合的所有元素都成立，则该表达式为真。现在，我们将考虑整数的集合。全称量词的例子，包装在一个断言中，如下所示:

method m()
{
   assert forall k :: k < k + 1;
}
   assert forall k :: k < k + 1;

量词为它所考虑的集合中的每个元素引入一个临时名称。这叫做绑定变量，在这里是k。绑定变量有一个类型，它几乎总是推断出来的，而不是显式给出的，而且通常是int。(一般来说，一个人可以有任意数量的绑定变量，这个主题我们将在后面返回。)一对冒号(::)将绑定变量及其可选类型与量化属性分隔开(量化属性的类型必须为bool)。在本例中，属性是对任何整数加1都是一个严格的更大的整数。Dafny能够自动证明这个简单的性质。一般来说，对无限集进行量化不是很有用，比如所有的整数。量词通常用于量化数组或数据结构中的所有元素。对于数组，我们可以使用隐含运算符，使得量化属性对于非索引的值很平凡地为真:

   assert forall k :: 0 <= k < a.Length ==> ...a[k]...;

这说明数组的每个元素都有一个属性。它的含义是，在计算表达式的第二部分之前，确保k实际上是数组中的有效下标。Dafny不仅可以使用这个事实来证明数组是安全访问的，而且还可以将必须考虑的整数集减少到只考虑数组中的下标。 对于量词，说明键不在数组中是很简单的:

   forall k :: 0 <= k < a.Length ==> a[k] != key

因此，我们的方法后置条件变成(加上a上的非零条件): method Find(a: array<int>, key: int) returns (index: int)

method Find(a: array<int>, key: int) returns (index: int)
   ensures 0 <= index ==> index < a.Length && a[index] == key
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
   // There are many ways to fill this in. Can you write one?
}
method Find(a: array<int>, key: int) returns (index: int)
   ensures 0 <= index ==> index < a.Length && a[index] == key
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
   ...
}

我们可以用多种方式填充这个方法的主体，但也许最简单的是线性搜索，实现如下:

method Find(a: array<int>, key: int) returns (index: int)
   ensures 0 <= index ==> index < a.Length && a[index] == key
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
   index := 0;
   while index < a.Length
   {
      if a[index] == key { return; }
      index := index + 1;
   }
   index := -1;
}
   index := 0;
   while index < a.Length
   {
      if a[index] == key { return; }
      index := index + 1;
   }
   index := -1;

正如您所看到的，我们在while循环中省略了循环不变量，因此Dafny在其中一个后置条件上给出了一个验证错误。我们得到错误的原因是Dafny不知道循环实际上覆盖了所有的元素。为了让Dafny相信这一点，我们必须编写一个不变式，说明当前索引之前的所有内容都已经被查看过了(并且不是键)。就像后置条件一样，我们可以使用一个量词来表达这个属性:

method Find(a: array<int>, key: int) returns (index: int)
   ensures 0 <= index ==> index < a.Length && a[index] == key
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
   index := 0;
   while index < a.Length
      invariant forall k :: 0 <= k < index ==> a[k] != key
   {
      if a[index] == key { return; }
      index := index + 1;
   }
   index := -1;
}
   invariant forall k :: 0 <= k < index ==> a[k] != key

这说明，除了之前的一切，当前的指数并不是关键。请注意，在进入循环时，i为零，因此隐含的第一部分总是假的，因此量化属性总是真的。这种常见的情况被称为空洞真理”:量词之所以成立，是因为它量化了一组空的对象。这意味着它在进入循环时为真。我们在扩展数组的非键部分之前测试数组的值，因此Dafny可以证明这个不变量是保留的。当我们试图添加这个不变量时，出现了一个问题:Dafny抱怨索引超出了不变量中数组访问的范围。 这段代码没有验证，因为在index上没有不变式，所以它可能大于数组的长度。那么绑定变量k可能会超过数组的长度。为了解决这个问题，我们将标准边界放在index上，0 <= index <= a.Length。注意，因为我们使用了k < index，所以即使在index == a.Length时，数组访问也不会出现错误。在处理数组时，使用超出增长范围末尾一处的变量是一种常见模式，在数组中，通常使用它每次构建一个元素的属性。完整的方法如下:

method Find(a: array<int>, key: int) returns (index: int)
   ensures 0 <= index ==> index < a.Length && a[index] == key
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
   index := 0;
   while index < a.Length
      invariant 0 <= index <= a.Length
      invariant forall k :: 0 <= k < index ==> a[k] != key
   {
      if a[index] == key { return; }
      index := index + 1;
   }
   index := -1;
}

练习12.

点击查看题目及代码

编写一个接受整数数组的方法，该方法要求数组至少有一个元素，并返回数组中最大元素的索引。用表示方法意图的前置和后置条件来注释方法，并用循环不变式来注释其主体以验证方法。

method FindMax(a: array<int>) returns (i: int)
   // Annotate this method with pre- and postconditions
   // that ensure it behaves as described.
{
   // Fill in the body that calculates the INDEX of the maximum.
}
method FindMax(a: array<int>) returns (i: int)

线性搜索不是很有效，特别是当许多查询由相同的数据组成时。如果数组是有序的，那么我们可以使用非常有效的二进制搜索过程来找到键。但是为了能够证明我们的实现是正确的，我们需要一些方法来要求输入的数组实际上是有序的。我们可以在方法的require子句中直接使用量词来实现这一点，但更模块化的表达方式是通过一个predicate。