前置和后置条件

到目前为止，我们所看到的所有代码都没有任何规范:代码几乎可以用任何命令式语言编写(适当考虑多个返回值)。Dafny的真正强大之处在于能够注释这些方法来指定它们的行为。例如，我们使用Abs方法观察到的一个属性是，不管输入是什么，结果总是大于或等于零。我们可以把这个观察结果放在注释中，但是我们没有办法知道这个方法是否真的有这个属性。而且，如果有人改变了方法，我们不能保证注释也会相应改变。通过注释，我们可以让Dafny证明我们声明的方法的属性是真的。有几种方法可以给出注解，但最常见和最基本的是方法的前置条件和后置条件。 Abs方法的这个属性，即结果总是非负的，是后置条件的一个例子:它是在方法返回后为真。用ensures关键字声明的后置条件，作为方法声明的一部分，在返回值之后(如果存在)和方法体之前给出。关键字后面跟着布尔表达式。像if或 while条件和大多数规范一样，后置条件总是一个布尔表达式:可以是true或 false. 在Abs方法的情况下，一个合理的后置条件如下:

method Abs(x: int) returns (y: int)
   ensures 0 <= y
{
   if x < 0 {
      return -x;
   } else {
      return x;
   }
}
method Abs(x: int) returns (y: int)
   ensures 0 <= y
{
   ...
}

你可以在这里看到为什么返回值被赋予名称。这使得它们很容易在方法的后置条件中引用。当表达式为真时，我们说后置条件保留。后置条件必须适用于函数的每次调用，以及每个可能的返回点 (包括函数体末尾的隐式返回点)。在这种情况下，我们唯一要表达的属性是返回值总是至少为零。 有时，我们需要为代码建立多个属性。在这种情况下，我们有两个选择。我们可以用布尔型的and操作符(&&), 将这两个条件连接起来，或者可以编写多个ensures表达式。后者与前者基本相同，但它区分了不同的属性。例如，MultipleReturns 方法的返回值名称可能会导致人们猜测以下后置条件:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
   ensures less < x
   ensures x < more
{
   more := x + y;
   less := x - y;
}

后置条件也可以这样写:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
   ensures less < x && x < more
{
   more := x + y;
   less := x - y;
}
   ensures less < x && x < more

甚至是这样：

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
   ensures less < x < more
{
   more := x + y;
   less := x - y;
}
   ensures less < x < more

因为Dafny中使用了链接比较运算符语法。(一般来说，大多数比较运算符可以串联，但只能同相连接，即不能混合使用大于和小于。详情请参阅参考资料。) 表示后置条件的第一种方式将less部分与more部分分开，这可能是可取的。另一件需要注意的事情是，我们在后置条件中包含了一个输入参数。这是有用的，因为它允许我们将方法的输入和输出相互关联(这是因为输入参数是只读的，所以在末尾和开始时是一样的)。 Dafny实际上拒绝了这个程序，声称第一个后置条件不成立 (即不为真)。这意味着Dafny不能证明该注释在每次方法返回时都有效。通常，Dafny验证错误有两个主要原因:规范与代码不一致，以及它不够聪明来证明所需属性的情况。区分这两种可能性可能是一项困难的任务，但幸运的是，Dafny和它所基于的Boogie/Z3系统非常聪明，并且将证明代码和规范的匹配非常简单。 在这种情况下，Dafny说代码有错误是正确的。问题的关键在于y是整数，所以它可以是负的。如果y为负(或为零)，那么more可以小于或等于x。除非y严格大于零，否则我们的方法将无法正常工作。这正是先决条件的概念。前置条件类似于后置条件，除了它必须在方法被调用之前为真。当您调用一个方法时，您的工作是建立(使)先决条件为真，这是Dafny使用证明来实现的。同样，当您编写一个方法时，您可以假定先决条件，但是您必须建立后置条件。然后，方法的调用者可以假定方法返回后置条件保持不变。 前提条件有自己的关键字requires。我们可以给予多次返回必要的先决条件如下:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
   requires 0 < y
   ensures less < x < more
{
   more := x + y;
   less := x - y;
}

与后置条件一样，多个前置条件可以用布尔型的and操作符(&&)或多个require关键字来写。传统上，源代码中的requires优先于ensure，尽管这并不是绝对必要的(尽管requires和ensure注释相对于其他同类型注释的顺序有时会很重要，我们将在后面看到)。添加了这个条件后，Dafny现在验证代码是否正确，只需要保证这个假设正确，就可以保证方法体中的代码是正确的。

练习0

点击查看题目及代码

编写一个方法Max，它接受两个整数参数并返回它们的最大值。添加适当的注释，并确保对代码进行验证。

method Max(a: int, b: int) returns (c: int)
  // What postcondition should go here, so that the function operates as expected?
  // Hint: there are many ways to write this.
{
  // fill in the code here
}
method Max(a: int, b: int) returns (c: int)

并不是所有的方法都有先决条件。例如，我们已经看到的Abs方法是为所有整数定义的，因此没有任何先决条件(除了它的参数是整数这一琐碎的要求，这是由类型系统强制执行的)。尽管它不需要先决条件，Abs函数目前的情况下并不是很有用。为了探究其中的原因，我们需要使用另一种注释，即断言。