dafny - 为什么需要这个微不足道的提示？

Question

我想知道为什么 Dafny 需要http://rise4fun.com/Dafny/8sl7中的注释提示 来验证断言？
有人可以解释一下吗？

Answer 1

原因是 Dafny 在构建证明时只愿意展开有限次数的函数。证明该断言需要展开 applyMapSeq 三次。

我建议在 applyMapSeq 中添加一些后置条件，这将有助于 Dafny 处理这个和其他证明。这是我想到的签名：

function applyMapSeq<U,V> (f: map<U,V>, xs:seq<U> ): (ys:seq<V>)
  requires (set x | x in xs) <= domain(f)
  ensures  |ys| == |xs|
  ensures  forall i :: 0 <= i < |xs| ==> ys[i] == f[xs[i]]

您可以在http://rise4fun.com/Dafny/Vibu看到，通过这些额外的后置条件，Dafny 可以验证您的断言。