
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:
Am I making a mistake somewhere or misunderstanding something ?
Many thanks
Alexis Chevalier



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

