要求在a中声明a [0]

问题描述

我目前正在学习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成立？

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

解决方法

这与“触发器”有关。

简短的答案是，除非您手动“提及” a[0]，否则Dafny将无法利用量化的requires子句。您提到a[0]的方式并不重要，只要您提及它即可。这就是为什么即使琐碎的断言似乎并没有在逻辑上添加任何内容的原因，它仍然起作用的原因：只是因为它提到了a[0]。

有关更多信息，请参见：

FAQ qustion
this answer“什么是触发器？”
this answer关于“找不到要触发的字词”

dafny