达夫尼：没有发现什么意思可以触发？

Question

我在达夫尼收到警告，说我的量词有

No terms found to trigger on.

我要为代码执行的操作是找到平方值小于或等于给定自然数'n'的最大数字。这是到目前为止我想到的代码：

method sqrt(n : nat) returns (r: int)
  // square less than or equal to n
  ensures (r * r) <= n 
  // largest number
  ensures forall i :: 0 <= i < r ==> (i * i) < (r * r)
{
    var i := 0; // increasing number
    r := 0;
    while ((i*i) <= n)
      invariant (r*r) <= n
      invariant forall k :: 0 <= k < r ==> (k*k) < (r*r)
      decreases n - i
    {
      r := i;
      i := i + 1;
    }

    return r;
}

在此代码段中，我通过使用post-condition验证是否返回的平方值小于或等于'n'的值ensures (r * r) <= n。

我还试图通过使用量词来验证返回的值的确是具有小于或等于'n'的平方值的最大值forall i :: 0 <= i < r ==> (i*i) < (r*r)

此量词表示所有在“ r”之前的元素的平方值小于r的平方值。

如何解决No terms found to trigger on.？这到底是什么意思？

达夫妮告诉我，这是一个警告。这是否表示我的量词有误？或这是否意味着Dafny根本无法验证它，但它是正确的？

Answer 1

该警告与Dafny（及其基础求解器Z3）如何处理量词有关。

首先，这确实是一个警告。如果程序没有错误（您的示例就是这种情况），则表明该程序已通过验证程序并满足其规范。您无需修复警告。

但是，在更复杂的程序中，您通常会发现警告伴随着失败或无法预测的验证结果。在那种情况下，值得知道如何修复它。通常，可以通过引入原本无用的辅助函数作为触发器来消除警告。

例如，这是您的示例的一个版本，其中Dafny不警告触发器

function square(n: int): int
{
    n * n
}

method sqrt(n : nat) returns (r: int)
  // square less than or equal to n
  ensures r * r <= n
  // largest number
  ensures forall i :: 0 <= i < r ==> square(i) < r * r
{
    var i := 0; // increasing number
    r := 0;
    while i * i <= n
      invariant r * r <= n
      invariant forall k :: 0 <= k < r ==> square(k) < r * r 
      decreases n - i
    {
      r := i;
      i := i + 1;
    }

    return r;
}

我所做的只是介绍一个square(n)定义为的新函数n * n，然后在程序其余部分中的一些关键位置使用它。

如果您只关心让这个示例进行验证，则可以在这里停止阅读。答案的其余部分试图解释为什么此修复程序起作用。

简而言之，之所以起作用，是因为Dafny现在可以使用square(i)和square(k)作为两个量词的触发器。

但是，什么是触发器，为什么是square(i)有效触发器却不i * i是？

什么是触发器？

触发器是涉及量化变量的句法模式，可作为求解器对量化器执行某些操作的试探法。使用forall量词，触发器会告诉Dafny何时使用其他表达式实例化量化公式。否则，Dafny将永远不会使用量化公式。

例如，考虑公式

forall x {:trigger P(x)} :: P(x) && Q(x)

在这里，注释{:trigger P(x)}会关闭Dafny的自动触发推论，并手动将触发条件指定为P(x)。否则，Dafny会同时推断出P(x)和Q(x)作为触发器，这通常通常更好，但对于解释触发器:)则更糟。

这个触发器意味着每当我们提到表单的表达式时P(...)，量词都会被实例化，这意味着我们...插入了for 的量词主体的副本x。

现在考虑这个程序

method test()
    requires forall x {:trigger P(x)} :: P(x) && Q(x)
    ensures Q(0)
{
}

Dafny抱怨无法验证后置条件。但这在逻辑上是显而易见的！只需插入0 x即可获取先决条件P(0) && Q(0)，这意味着后置条件Q(0)。

由于我们选择了触发器，Dafny无法验证此方法。由于后置条件仅提及Q(0)，而没有涉及P，而量词仅由触发P，Dafny将永远不会实例化该前提条件。

我们可以通过添加看似无用的断言来修复此方法

assert P(0);

到方法的主体。现在将验证整个方法，包括后置条件。为什么？因为我们提到过P(0)，它从前置条件触发了量词，导致求解器学习P(0) && Q(0)，从而可以证明后置条件。

花一点时间，了解发生了什么。我们有一个逻辑上正确但未能通过验证的方法，并向其添加了一个逻辑上无关但真实的断言，从而使验证程序突然获得成功。换句话说，达夫尼的验证者有时可能依赖于逻辑上不相关的影响才能成功，尤其是在涉及数量词时。

成为合格的Dafny用户的重要组成部分，是了解何时可以通过逻辑上不相关的影响来解决故障，以及如何找到正确的方法来说服Dafny成功。

（顺便说一句，请注意，如果我们让Dafny推断触发器而不是手动进行触发，则本示例将在不相关声明的情况下进行。）

什么才是好的触发条件？

好的触发器通常是包含不涉及所谓“解释符号”的量化变量的小表达式，就我们的目的而言，可以将其视为“算术运算”。触发器中不允许使用算术，这有一个很好的理由，即求解器无法轻松分辨何时提到了触发器。例如，如果x + y是允许的触发器，而程序员提到(y + 0) * 1 + x，则求解器将很难立即意识到这等于触发器表达式。由于这可能导致量词的实例化不一致，因此触发器中不允许进行算术运算。

许多其他表达式被允许作为触发器，例如索引为Dafny数据结构，提领域，组成员资格，和功能应用。

有时，最原始的公式公式就像原始示例一样，不包含任何有效触发器。在这种情况下，Dafny会警告您。有时，无论如何验证都会成功，但是在大型程序中，您通常需要修复这些警告。一个好的通用策略是在量化公式的某些部分的摘要中引入一个新函数，以作为触发器。