终止

Dafny中的关键字predicate表示函数终止。

下面是一个奇偶校验的例子。对于正整数n，当n为偶数时对n - 1进行奇校验，当n为奇数时对n - 1进行偶校验。当n减小到0时，若为偶校验调用则返回真，为奇校验调用则返回假。

predicate even(n: nat)  // 偶校验
   ensures even(n) <==> n % 2 == 0
{
   if n == 0 then true else odd(n-1)
}

predicate odd(n: nat)   //奇校验
   ensures odd(n) <==> n % 2 != 0
{
   if n == 0 then false else even(n-1)
}

上述两个方法缺一不可，因为它们要达到终止条件就必须互相调用直至其中一个方法递归返回。