Array to Sequence to Multisets and comparison

Jul 7, 2016 at 9:56 PM
Hello, I am a student working on my MSc dissertation and I use dafny to specify a data structures/algorithms library. I am currently trying a Insertion sort implementation, and I am using the multisets in order to validate the permutation of my array, but I don't understand the behavior of the verifier for the following code:
class Test {
  method Main()
  {
    var arrInt := new int[5];
    arrInt[0] := 4;
    arrInt[1] := 3;
    arrInt[2] := 2;
    arrInt[3] := 1;
    arrInt[4] := 0;

    var m1 := multiset(arrInt[..]);
    var m2 := multiset([4,3,2,1,0]);
    assert m1 == m2; //The assertion is violated
  }
}
I am trying to check that the multiset m1, obtained from an array transformed in a sequence and then in a multiset (Maybe I'm doing this the wrong way) is the exact same than the multiset m2, obtained from a valid sequence (at least I think).

The debugger also give weird values for the multiset m1:
Image

Am I making a mistake somewhere or misunderstanding something ?

Many thanks
Alexis Chevalier
Jul 8, 2016 at 1:35 PM
Hello,

I made some changes in my program this morning, I had not realized that the state of the array needed to be asserted before trying to use it, this version is now accepted by the verifier:
class Test {
  method Main()
  {
    var arrInt := new int[5];
    arrInt[0] := 4;
    arrInt[1] := 3;
    arrInt[2] := 2;
    arrInt[3] := 1;
    arrInt[4] := 0;
    
    assert arrInt[..] == [4,3,2,1,0]; //Assertion of the array's sequence

    var m1 := multiset(arrInt[..]);
    var m2 := multiset([4,3,2,1,0]);
    assert m1 == m2; //The assertion is now valid
  }
}
Sorry for the disturbance,
Alexis Chevalier
Marked as answer by AlexisChevalier on 7/8/2016 at 5:44 AM