dafny - 需要在 a 中断言 a[0]

Question

我目前正在学习 dafny 并遇到了一个非常奇怪的断言要求：

method M (a : seq<int>, acc : seq<int>) 
  requires |a| > 0
  requires forall va, vacc :: va in a && vacc in acc ==> vacc <= va
{
  assert forall vacc :: vacc in acc ==> vacc <= a[0];
}

上面的代码在断言上失败了，但是如果我添加assert a[0] in a它验证？

为什么会出现这种情况，肯定在所有情况下都|a| > 0 a[0] in a成立，因为seq它是不可变的？

（也将不胜感激任何风格指南建议:)）

标签： dafny

Answer 1

这与“触发器”有关。

简短的回答是，除非您手动“提及” a[0]，否则 Dafny 将无法利用量化requires子句。你怎么提都没关系a[0]，只要你提就行了。这就是为什么即使您的琐碎断言在逻辑上似乎没有添加任何内容，但它仍然有效：这只是因为它提到了a[0].

有关更多信息，请参阅：

• 常见问题解答
• 这个答案“什么是触发器？”
• 这个关于“没有找到触发条件”的答案