Dafny多集

Question

在参考手册(http://www.cse.unsw.edu.au/~se2011/DafnyDocumentation/Dafny%20-%20ValueTypes.pdf)中，我们可以发现:如果两个多集对每个元素的计数完全相同，则它们是相等的。然而，如果我断言：

   assert multiset({1,1}) == multiset{1};

所以我理解了一些不对劲的地方。

例如，为了证明这一点：

lemma seqSplit(s:seq<int>, c:int, p:int, f:int)
       requires 0<=c<=p<=f+1<=|s|
       ensures multiset(s[c..f+1]) == multiset(s[c..p])+multiset(s[p..f+1])

什么是必要的？我一开始是：

       assert forall i :: c<=i<=f ==> 
              (s[i] in multiset(s[c..f+1]) <==> (s[i] in multiset(s[c..p]) || s[i] in multiset(s[p..f+1])));

它验证了，我想说，它与“确保”中的内容相同，但似乎并非如此。有什么帮助吗？

Answer 1

multiset({1,1})的意思是“构造集合{1,1}，然后将其转换为多集”。由于set {1,1}和set {1}是相同的，所以您的断言会传递。

我想你想要multiset{1,1}。