Dafny: assertion needed for verification to go through

Nov 7, 2012 at 8:28 AM


I could persuade Dafny of the correctness of a selection sort algorithm. However, I seem to need certain assert statement in the main loop or otherwise it fails. I'm guessing that the verification of the assertion is firing some required trigger. Is my understanding correct? In any case, is there a simple way to "fix" this example?

The relevant code is here: http://rise4fun.com/Dafny/vuD9


Mar 26, 2014 at 9:57 PM
I was having a similar problem; I replaced the multiset invariant and post-condition with the post condition

ensures exists j:multiset<int> :: j == multiset(old(a[..]) ==> multiset(a[..]);

Afterwards, the ghost var/assertion was not needed.

I hope this will solve the problem you were having.