达夫尼：没有发现什么意思可以触发？ [英] Dafny: What does no terms found to trigger on mean?
问题描述
我在达夫尼（Dafny）得到警告，说我的量词有
未找到触发条件。
我要为代码执行的操作是找到平方值小于或等于给定自然数'n'的最大数字。这是到目前为止我想出的代码：
方法sqrt（n：nat）返回（r：int）
//小于或等于n的平方
确保（r * r）< = n
//最大数
确保所有i :: 0< = i< r ==> （i * i）< （r * r）
{
var i：= 0; //增加数字
r：= 0;
而（（i * i）< = n）
不变（r * r）< = n
不变k全部为k :: 0< = k< r ==> （k * k）< （r * r）
减少n-i
{
r：= i;
i：= i + 1;
}
return r;
}
在此代码段中，我正在验证我返回的值是否为通过使用后置条件确保（r * r）< = n 来小于或等于'n'的平方值。
我也在尝试，以验证返回值的确是平方值小于或等于'的最大值。通过使用量词 forall i'n'：0< = i< r ==> （i * i）< （r * r）
此量词表示 r之前的所有元素的平方值小于平方值
如何解决未找到要触发的条件。？这到底是什么意思？
Dafny告诉我这是一个警告。这是否表示我的量词有误？还是这意味着Dafny根本无法验证它，但它是正确的？
警告与Dafny（和基础求解器Z3）处理量词。
首先，这确实是一个警告。如果程序没有错误（您的示例就是这种情况），则表明该程序已通过验证程序并满足其规范。您不需要修正警告。
但是，在更复杂的程序中，您常常会发现警告伴随着失败或无法预测的验证结果。在这种情况下，值得一试。通常，可以通过引入其他没用的辅助函数作为触发器来消除警告。
例如，这是您的示例的一个版本，其中Dafny不警告触发器
函数平方（n：int）：int
{
n * n
}
方法sqrt（n：nat）返回（r：int）
//小于或等于n的平方
确保r * r< = n
//最大数
确保所有i :: 0< = i< r ==>平方（i）< r * r
{
var i：= 0; //增加数字
r：= 0;
而i * i <= n
不变r * r <= n
不变k全部为k :: 0< = k< r ==>平方（k）< r * r
减少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（...）形式的表达式，量词就会得到 instantiated ，这意味着我们可以插入 ... 的量词主体的副本，而 x 。
现在考虑该程序
方法test（）
需要全部x {：trigger P（x）} :: P（x）&& Q（x）
确保Q（0）
{
}
Dafny抱怨无法验证后置条件。但这在逻辑上是显而易见的！只需将 x 插入0，即可获得 P（0）&& Q（0），这意味着后置条件 Q（0）。
Dafny无法验证此方法，因为我们选择了触发器。由于后置条件仅提及 Q（0），而没有提及 P ，因此量词仅由<$触发c $ c> P ，Dafny永远不会实例化前提条件。
我们可以通过添加看似无用的断言来修复此方法
断言P（0）;
方法的主体。现在将验证整个方法，包括后置条件。为什么？因为我们提到了 P（0），它从前提条件中触发了量词，导致求解器学习了 P（0）&& Q（0），从而可以证明后置条件。
花点时间了解一下发生了什么。我们有一个逻辑上正确但未能通过验证的方法，并向其添加了一个逻辑上无关但真实的断言，从而使验证程序突然获得成功。换句话说，达夫尼的验证者有时可能要依靠逻辑上不相关的影响才能取得成功，尤其是在涉及数量词的情况下。
Dafny用户了解何时可以通过逻辑上不相关的影响来解决故障，以及如何找到正确的方法来说服Dafny成功。
（顺便说一句，请注意，如果我们让Dafny推断触发器而不是手动对其进行触发，则该示例将在不相关声明的情况下进行。）
什么是好的触发器？
好的触发器通常是包含不涉及所谓解释符号的量化变量的小表达式，就我们的目的而言，可以将其视为算术运算。触发器中不允许使用算术，这有一个很好的理由，即求解器无法轻松分辨何时提到了触发器。例如，如果 x + y 是允许的触发器，并且程序员提到（y + 0）* 1 + x ，求解器将很难立即意识到这等于触发表达式。由于这可能导致量词的实例化不一致，因此触发器中不允许进行算术运算。
许多其他表达式 都可以用作触发器，例如索引到Dafny中数据结构，取消引用字段，集合成员资格和函数应用程序。
有时候，写下公式的最自然的方法将不包含有效的触发器，就像您的原始示例一样。在这种情况下，Dafny会警告您。有时，无论如何验证都会成功，但是在大型程序中，您通常需要修复这些警告。一个好的通用策略是在量化公式的某些部分的摘要中引入一个可以用作触发器的新函数。
I am getting a warning in Dafny which says that my quantifiers have
No terms found to trigger on.
What I am trying to do for my code is to find the largest number that has a square value that is less than or equal to the given natural number 'n'. Here is the code I came up with so far:
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;
}
In this snippet, I am verifying that I am returning a value that has a square value which is less than or equal to 'n' by using the post-condition ensures (r * r) <= n.
I am also trying to verify that the returned value is indeed the largest value that has a square value that is less than or equal to 'n' by using the quantifier forall i :: 0 <= i < r ==> (i*i) < (r*r)
This quantifier means that all elements which came before 'r' has a square value that is smaller than the square value of r.
How does one fix the No terms found to trigger on.? What does it actually mean?
Dafny tells me that it is a warning. Does this mean that my quantifiers are wrong? or Does it mean that Dafny cannot verify it at all but it is correct?
The warning has to do with how Dafny (and the underlying solver Z3) handle quantifiers.
First of all, it truly is a warning. If the program has no errors (which is the case for your example), then it has passed the verifier and satisfies its specification. You don't need to fix the warning.
However, in more complex programs you will often find that the warning comes along with failed or unpredictable verification outcomes. In those cases, it's worth knowing how to fix it. Often, the warning can be eliminated by introducing a otherwise-useless helper function to serve as the trigger.
For example, here is a version of your example where Dafny does not warn about triggers
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;
}
All I did was introduce a new function square(n) defined to be n * n, and then used it in a few key places under quantifiers in the rest of the program.
If all you care about is getting this one example to verify, you can stop reading here. The rest of the answer tries to explain why this fix works.
In short, it works because Dafny is now able to use square(i) and square(k) as triggers for the two quantifiers.
But, what is a trigger anyway, and why is square(i) a valid trigger but i * i isn't?
What is a trigger?
A trigger is a syntactic pattern involving quantified variables that serves as heuristic for the solver to do something with the quantifier. With a forall quantifier, the trigger tells Dafny when to instantiate the quantified formula with other expressions. Otherwise, Dafny will never use the quantified formula.
For example, consider the formula
forall x {:trigger P(x)} :: P(x) && Q(x)
Here, the annotation {:trigger P(x)} turns off Dafny's automatic trigger inference and manually specifies the trigger to be P(x). Otherwise, Dafny would have inferred both P(x) and Q(x) as triggers, which is typically better in general, but worse for explaining triggers :).
This trigger means that whenever we mention an expression of the form P(...), the quantifier will get instantiated, meaning that we get a copy of the body of the quantifier with ... plugged in for x.
Now consider this program
method test()
requires forall x {:trigger P(x)} :: P(x) && Q(x)
ensures Q(0)
{
}
Dafny complains that it cannot verify the postcondition. But this is logically obvious! Just plug in 0 for x in the precondition to get P(0) && Q(0), which implies the postcondition Q(0).
Dafny cannot verify this method because of our choice of triggers. Since the postcondition mentions only Q(0), and nothing about P, but the quantifier is triggered only by P, Dafny will never instantiate the precondition.
We can fix this method by adding the seemingly-useless assertion
assert P(0);
to the body of the method. The whole method now verifies, including the postcondition. Why? Because we mentioned P(0), which triggered the quantifier from the precondition, causing the solver to learn P(0) && Q(0), which allows it to prove the postcondition.
Take a minute and realize what just happened. We had a logically-correct-but-failing-to-verify method and added a logically-irrelevant-but-true assertion to it, causing the verifier to suddenly succeed. In other words, Dafny's verifier can sometimes depend on logically-irrelevant influences in order to succeed, especially when there are quantifiers involved.
It is an essential part of becoming a competent Dafny user to understand when a failure can be fixed by a logically-irrelevant influence, and how to find the right trick to convince Dafny to succeed.
(As an aside, note that this example goes through without the irrelevant assertion if we let Dafny infer triggers instead of manually hobbling it.)
What makes a good trigger?
Good triggers are usually small expressions containing the quantified variables that do not involve so-called "interpreted symbols", which, for our purposes, can be considered "arithmetic operations". Arithmetic is not allowed in triggers for the good reason that the solver cannot easily tell when a trigger has been mentioned. For example, if x + y was an allowed trigger and the programmer mentioned (y + 0) * 1 + x, the solver would have trouble immediately recognizing that this was equal to a triggering expression. Since this can cause inconsistent instantiation of quantifiers, arithmetic is disallowed in triggers.
Many other expressions are allowed as triggers, such as indexing into Dafny data structures, dereferencing fields, set membership, and function application.
Sometimes, the most natural way of writing down a formula will contain no valid triggers, as your original example did. In that case, Dafny will warn you. Sometimes, verification will succeed anyways, but in large programs you will often need to fix these warnings. A good general strategy is to introduce a new function the abstract some part of the quantified formula that can serve as a trigger.
这篇关于达夫尼：没有发现什么意思可以触发？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
