Conversion from sequences to multisets

May 20, 2014 at 11:07 PM
The code below does not succeed without the helper assertions--which renders unusable the conversion from sequences to multisets. Am I missing something?

method Test()
{
var a: seq<int> := [0,11,22,33,33,55,66,77,88];
var b: seq<int> := [22,33,9,9,9,9,33];

var s1: seq<int> := a[2..5];
/ why needed?? / assert s1 == [22,33,33];
assert multiset(s1) == multiset{22, 33, 33};
var sR1: seq<int> := b[..2];
/ why needed?? / assert sR1 == [22,33];
assert multiset(sR1) == multiset{22, 33};
var sR2: seq<int> := b[6..];
// did not need! / assert sR2 == [33];
assert multiset(sR2) == multiset{33};
assert multiset(s1) == multiset(sR1) + multiset(sR2);
}
May 21, 2014 at 2:51 PM
My question is actually about slicing:

method TestSeqFromSubArray(a: array<int>, b: int, e: int)
requires a != null;
requires 0 <= b < e <= a.Length;
{
var s := a[b..e];
//Why a violation? assert a[b] in s;
//Even this is a violation: assert !(a[b] in s);
}