Dafny：没有找到触发的术语是什么意思？答案

【问题标题】：Dafny: What does no terms found to trigger on mean?Dafny：没有找到触发的术语是什么意思？
【发布时间】：2018-08-30 02:52:03
【问题描述】：

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

在这个 sn-p 中，我通过使用后置条件 ensures (r * r) <= n 来验证我正在返回一个平方值小于或等于“n”的值。

我也尝试使用量词forall i :: 0 <= i < r ==> (i*i) < (r*r)验证返回值确实是平方值小于或等于“n”的最大值

这个量词意味着所有在 'r' 之前的元素的平方值都小于 r 的平方值。

如何修复No terms found to trigger on.？它实际上是什么意思？

Dafny 告诉我这是一个警告。这是否意味着我的量词是错误的？或者这是否意味着 Dafny 根本无法验证它但它是正确的？

【问题讨论】：

标签： formal-verification dafny

【解决方案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 何时用其他表达式实例化量化公式。否则，达夫尼永远不会使用量化公式。

例如，考虑公式

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 用户的重要组成部分。

（顺便说一句，请注意，如果我们让 Dafny 推断触发器而不是手动阻止它，则此示例没有无关的断言。）

什么是好的触发器？

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

许多其他表达式被允许作为触发器，例如对 Dafny 数据结构的索引、取消引用字段、集合成员资格和函数应用程序。

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

【讨论】：