in 运算符，用于在 Dafny 中比较奇怪的序列答案

【问题标题】：in operator for sequences comporting weird in Dafnyin 运算符，用于在 Dafny 中比较奇怪的序列
【发布时间】：2019-09-29 19:49:06
【问题描述】：

我如何帮助 Dafny 证明以下两个断言是相同的：

method foo(xs : seq<int>)
  requires forall x :: x in xs ==> 0 <= x < 5;
{
  assert forall x :: x in xs ==> 0 <= x < 5;
  assert forall i :: 0 <= i < |xs| ==> 0 <= xs[i] < 5;
}

此外，Dafny 似乎能够证明以下内容是相同的。这是为什么呢？


predicate test(value : int) {
  0 <= value < 5
}

method foo'(xs : seq<int>)
  requires forall x :: x in xs ==> test(x);
{
  assert forall i :: 0 <= i < |xs| ==> test(xs[i]);
}

Example on Rise4Fun

【问题讨论】：

标签： seq dafny

【解决方案1】：

这与量词触发器有关。您可以在Dafny FAQ 中阅读有关触发器的更多信息。

在这种情况下，第一个示例中最终断言失败的原因是requires 子句和第一个断言中的forall 量词是在x in xs 上触发的。¹ 这个意味着这个量化的事实不会在值v 处使用，除非v in xs 在验证者的“范围内”。为了证明第二个断言，验证者需要使用值 xs[i] 的较早量化事实，但 xs[i] in xs 不在“范围内”。这听起来可能很奇怪，因为xs[i] in xs 总是正确的，但事实证明，如果没有您的帮助，验证者无法解决这个问题。

因此，为了证明第二个断言，您需要以某种方式在范围内获取事实 xs[i] in xs。一种方法是将断言更改为

assert forall i :: 0 <= i < |xs| ==> xs[i] in xs && 0 <= xs[i] < 5;

（在结论中添加xs[i] in xs）。事实上，一旦这个新断言被证明，Dafny 就可以然后证明你的第二个断言，因为这个新断言是在 xs[i] 上触发的，这也是你第二个断言的“范围内”。

最后，您的第二个示例验证的原因是因为引入谓词 test 已经改变了可用的触发器。现在requires 子句中的forall 在x in xs 和 test(x) 上都被触发。新触发器与foo 正文中的新版本断言匹配，因为test(xs[i]) 已经出现。这会导致第一个forall 被正确实例化，这意味着断言通过。在按摩触发器以让它们做你想做的事情时，引入这样的无用命名谓词是一个常见的技巧。

1. 您可以通过将鼠标悬停在 IDE 中的 forall 上，或者通过在命令行上运行选项 /printTooltips 来查看正在使用的触发器。对于第一个示例中的第一个断言，您应该看到类似 Selected triggers: {x in xs} 的内容。

【讨论】：