谓词

谓词是一个返回布尔值的函数。这是一个简单但强大的想法，发生在Dafny的程序。例如，我们将整数数组上的sorted谓词定义为一个函数，该函数接受一个数组作为参数，当且仅当该数组按递增顺序排序时，返回true。谓词的使用使我们的代码更短，因为我们不需要一遍又一遍地写出一个很长的属性。它还可以通过给一个公共属性命名来使我们的代码更容易阅读。 我们有很多方法可以写sorted谓词，但最简单的是在数组的下标上使用一个量词。我们可以写一个量词来表示属性“如果数组中x在y之前，那么x <= y，作为一个量词在两个绑定变量上:

   forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]

这里我们有两个绑定变量，j和k，都是整数。两者之间的比较保证了它们在数组中都是有效的下标，并且j在k之前。然后第二部分说它们彼此之间的顺序是正确的。量词在Dafny中只是一种布尔值表达式，所以我们可以将排序谓词写为:

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

注意，没有返回类型，因为谓词总是返回布尔值。 Dafny拒绝给出的这段代码，声称谓词读不出a。修复此问题需要另一个注释，读取注释。