爲什麼這個瑣碎的提示是必需的？

Question

我想知道爲什麼Dafny需要http://rise4fun.com/Dafny/8sl7 中的註釋提示來驗證斷言？
有人可以解釋嗎？

Answer 1

原因是Dafny只在構造證明時只願意展開函數有限次數。證明斷言需要展開applyMapSeq三次。

我建議添加一些後置條件來應用MapSeq，這將有助於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可以驗證你的說法。