问题描述
在参考手册 (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])));
它验证了,我会说它与确保中的相同,但似乎不是。有什么帮助吗?
解决方法
multiset({1,1})
表示“构造 set {1,1}
,然后将其转换为多重集”。由于集合 {1,1}
和集合 {1}
相同,因此您的断言通过。
我想你想要multiset{1,1}
。