大夫。没有发现触发的条件是什么意思?[英] Dafny: What does no terms found to trigger on mean?

本文是小编为大家收集整理的关于大夫。没有发现触发的条件是什么意思?的处理方法,想解了大夫。没有发现触发的条件是什么意思?的问题怎么解决?大夫。没有发现触发的条件是什么意思?问题的解决办法?那么可以参考本文帮助大家快速定位并解决问题。

问题描述

我在 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)

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

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

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

推荐答案

警告与 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;
}

我所做的只是引入一个定义为 n * n 的新函数 square(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 会警告您.有时,无论如何验证都会成功,但在大型程序中,您通常需要修复这些警告.一个好的通用策略是引入一个新函数,将量化公式的某些部分抽象为触发器.

本文地址:https://www.itbaoku.cn/post/1793854.html