formal-verification - 达夫尼:没有发现什么意思可以触发？

Question

我在达夫尼（Dafny）得到警告，说我的量词有

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;
}

在此代码段中，我正在验证是否使用后置条件 ensures (r * r) <= n返回的平方值小于或等于'n'的值。

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

此量词表示所有在“ 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(...)的表达式，量词都会被实例化，这意味着我们将为 ...插入 x来获取量词主体的副本。

现在考虑这个程序

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

Dafny抱怨无法验证后置条件。但这在逻辑上是显而易见的！只需在前置条件中为 x插入0即可获得 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会警告您。有时，验证还是会成功，但是在大型程序中，您通常需要修复这些警告。一个好的通用策略是在量化公式的某些部分的摘要中引入一个可以用作触发器的新函数。