自动调用引理

K. Rustan M. Leino Manuscript KRML 265, 8 June 2019

摘要 函数的某些性质比其他性质更有用。如果你已经证明了这样一个性质作为一个引理，你可能想让它自动应用。本文将讨论在Dafny中实现这类目标的方法。

在https://github.com/Microsoft/dafny/issues/231 (opens new window)上，一名Dafny用户问道:

有一种方法在Dafny标记一个引理为“自动”，并将其添加到z3的知识库?

对于学生的家庭作业，我们经常会遇到一些对于Dafny来说过于复杂的规范，并且需要一些手工制作的断言或引理。

如果我们能够定义那些引理来用特定领域的知识来扩充boogie/z3搜索空间，那就太好了，这样我们就不必向学生解释引理是如何工作的，以及查找和使用所需引理的繁琐和困难的任务。

类似于{:auto}注释的东西是可行的吗?我们能否增强。bpl的公理化?

下面的例子说明了这个问题。假设你声明了一个函数，并证明了它的属性:

function FibFib(n: nat): nat {
  if n == 0 then 0
  else if n == 1 then 2
  else FibFib(n-2) + FibFib(n-1)
}

lemma FibFibIsEven(n: nat)
  ensures FibFib(n) % 2 == 0
{
  // automatically proved by induction
}

对于您的应用程序，FibFib总是返回一个偶数可能是至关重要的。使用上面的声明，你将不得不在每次使用函数时调用引理FibFibIsEven。这是乏味的。是否有一些方法来指示Dafny自动应用FibFibIsEven当它需要的时候?

不，Dafny没有这样的特色。(例如，VCC就有这样一个功能。)在某些情况下，这种自动化可能工作得很好。在其他情况下，它可能会导致引理被调用太多次(比如，无限次)，这是有问题的。

如果您有兴趣尝试一些{:autoLemma}特性，请随意使用开放的Dafny源代码。在目前的状态下，我有四个建议你可以尝试，这些建议可能会减轻你正在经历的一些乏味。

超级引理

一个建议是创建一个“超级引理”来收集其他几个引理的陈述。例如，如果你已经有了:

lemma Lemma0(x: X) ensures P0(x) { ... }
lemma Lemma1(x: X) ensures P1(x) { ... }
lemma Lemma2(x: X) ensures P2(x) { ... }

然后你可以把它们合并成一个:

lemma Everything(x: X)
  ensures P0(x) && P1(x) && P2(x)
{
  Lemma0(x: X);
  Lemma1(x: X);
  Lemma2(x: X);
}

这让您可以通过调用一个引理来获得所有3个属性。

聚合引理调用

另一个建议是在同一时间对多个值调用引理。考虑到:

lemma LemmaForOneX(x: X) ensures P(x) { ... }

你可以对X的所有值同时调用这个引理:

forall x {
  LemmaForOneX(x);
}

通过把这个forall语句放在你要证明的一些代码的开头，你实际上已经为每一个可能的X值调用了它。当然，你也可以把这个表述放入一个引理中，然后称之为这个引理:

lemma LemmaForEveryX()
  ensures forall x :: P(x)
{
  forall x {
    LemmaForOneX(x);
  }
}

在许多情况下，这将很好地工作。在其他情况下，验证者可能没有意识到你调用了需要单个引理的值上的引理，所以你可能仍然需要手动调用LemmaForOneX。此外，Dafny还采取措施避免在为上面的引理调用生成的量词中出现“匹配循环”(“匹配循环”会导致引理的无限次使用)。然而，这种机制并不完美，因此这种增加的自动化在某些情况下可能会导致性能下降。

函数后置条件

第三个建议是在函数的后置条件中声明函数的一些最有用的属性，而不是在单独的引理中声明。例如，代替:

function F(x: X): int { ... }
lemma AboutF(x: X)
  ensures F(x) % 2 == 0
{ ... }

你可以声明为：

function F(x: X): int
  ensures F(x) % 2 == 0
{ ... }

要获得引理所声明的属性，必须调用引理。相反，在函数的后置条件中声明的任何属性都会在每次调用函数时自动应用。

正如我所提到的，更多的信息可以帮助验证者自动地做更多的事情，但是过多的信息也会让验证者不知所措。因此，我的建议是只对那些您认为每个函数用户都需要的属性使用函数后置条件。很少需要的属性最好在必须手动调用的引理中声明。

此外，在函数后置条件中可以编写的内容也有限制。特别是，你写的东西必须“终止”。在实践中，这意味着在后置条件中提到函数应用于其他参数时可能会遇到问题。例如,

predicate R(x: X, y: X)
  // commutativity:
  ensures R(x, y) <==> R(y, x)
  // transitivity:
  ensures forall z :: R(x, z) && R(z, y) ==> R(x, y)

不被允许，因为后置条件中存在自引用非终止(即无限递归)调用。因此，像交换性和及物性这样的性质总是需要表述为独立的引理。

基本/高级函数对

函数后置条件方便地为函数的所有用户提供它所声明的属性，从而减少了显式调用引理的需要。如果不是所有用户都对该属性感兴趣，那么第四个建议是声明两个函数。基本函数给出了函数的实际定义，附带的引理说明了它的性质。premium函数调用基本函数并将属性声明为后置条件，这是通过调用引理来证明的。

function F(x: X): int { ... }
lemma AboutF(x: X)
  ensures F(x) % 2 == 0
{ ... }

function F_premium(x: X): int
  ensures F_premium(x) % 2 == 0
{ AboutF(x); F(x) }

用户现在可以选择:调用F_premium可以获得函数的值和被证明的属性，而调用F只能获得函数的值。如果你希望高级版本比基础版本更受欢迎，你当然可以将F和F_premium分别重命名为F_basic和F。

除了后置条件之外，这两个函数是同义词。语义。需要注意的是，验证器用来指导其量词使用的机制是语法上的。因此，当验证者决定实例化量词时，你在量词主体中使用的两个函数中的哪一个可以产生差异。出于这个原因，我建议您在编写的任何量词中使用函数的基本版本。

致谢

Bryan Parno提出了第四个建议，将函数的基本版本及其引理包装成函数的高级版本。