1

我在使用 VS 的 Dafny 插件时收到以下警告消息。谁能解释一下这是什么意思？

Selected triggers: {a[i]} (may loop with "a[i + 1]"). Suppressing loops would leave this expression without triggers.

有问题的行是

assert forall i : int :: 0<=i<a.Length-1 ==> a[i] <= a[i+1] ;

另外，由于这只是一条警告消息，我是否可以断定验证是否成功？

4

1 回答 1

1

首先，你是对的，如果没有其他错误报告，那么你可以断定验证成功。

该警告与 Z3（以及 Dafny）如何通过基于启发式模式的实例化处理量词有关。消息是说 Dafny 已决定选择a[i]作为此量词的触发器（模式），即使它有一个所谓的“匹配循环”与a[i+1]. Dafny 决定这样做是因为它觉得它没有其他选择作为触发器。

请注意，全称量词上的模式仅在稍后使用量化事实时才相关，而不是在证明它时。通过在由模式确定的具体值上实例化它来使用普遍量化的事实。（双重地，存在量词上的模式仅在证明它们时才相关；通过尝试使用与模式匹配的值作为见证来证明存在量词。）

当使用与模式匹配的值实例化量词时，通用量词上的模式会导致匹配循环，这会导致构造另一个不同的值。对于您的示例，该模式意味着“任何时候您在上下文中浮动a[i]形式的表达式，尝试通过插入for 来实例化量词。假设值在上下文中浮动。然后量词将被实例化为产生基本条款a[blah]blaha[i]a[0]i == 0

0 <= i < a.Length - 1 ==> a[0] <= a[1]

这个新子句被添加到上下文中，并包含值a[1]，它也与模式匹配。所以求解器可能会再次实例化量词，这将导致值a[2]被添加到上下文中。这可能会永远持续下去并降低求解器的性能。

使用像 Dafny 这样的工具的一部分艺术是设计公式以避免匹配循环。此公式的一种解决方法是将其重写为

forall i, j :: 0 <= i <= j < a.Length - 1 ==> a[i] <= a[j]

由于<=是传递的，这在逻辑上等价于前面的公式。但是当模式是时它没有匹配循环{a[i], a[j]}（有两个量化变量，因此需要扩展模式以包含它们），因为用特定值实例化它不会创建与模式匹配的新值。

此公式的另一个解决方法是

forall i, j :: 0 <= i <= j < a.Length - 1 && j == i+1 ==> a[i] <= a[j]

这个公式在逻辑上也等同于第一个公式，因为它被限制j为 的同义词i+1。虽然这似乎是一种奇怪的编写方式，但它也消除了循环。

事实上，现代版本的 Dafny 会透明地将您的原始公式重写为最后一个公式，以消除循环并避免警告。

于 2017-10-08T22:27:18.917 回答