i am new in Dafny and i have problems verifying my insertionSort-implementation. Dafny tells me the the multiset invariants are not holding, anything else is working fine. After Hours of searching the mistake i could need some help :) Would be nice if somebody could tell me the trick!
My Code:
predicate sorted(a:array<int>, min:int, max:int)
requires a != null;
requires 0<= min <= max <= a.Length;
reads a;
{
forall j, k :: min <= j < k < max ==> a[j] <= a[k]
}
/*
*
*/
method insertionSort(a: array<int>)
requires a != null;
requires a.Length > 0;
ensures sorted(a, 0, a.Length);
ensures multiset(a[..]) == multiset(old(a[..]));
modifies a;
{
var i := 1;
while(i < a.Length)
invariant 1 <= i <= a.Length;
invariant sorted(a, 0, i);
invariant a != null;
invariant multiset(old(a[..])) == multiset(a[..]);
decreases a.Length-i;
{
var j := i - 1;
var key := a[i];
while(j >= 0 && key < a[j])
invariant -1 <= j <= i - 1 <= a.Length;
invariant (j == i-1 && sorted(a, 0, i)) || (sorted(a, 0, i+1));
invariant forall k :: j < k < i ==> a[k] >= key;
invariant -1 < j == i - 1 ==> multiset(old(a[..])) == multiset(a[..]);
invariant |multiset(old(a[..]))| == |multiset(a[..])|;
invariant -1 < j < i - 1 && key < a[j] ==> multiset(old(a[..])) == multiset(a[..]) - multiset({a[j+1]}) + multiset({key});
invariant -1 == j ==> multiset(old(a[..])) == multiset(a[..]) + multiset({key}) - multiset({a[j+1]});
decreases j;
{
a[j + 1] := a[j];
j := j - 1;
}
a[j + 1] := key;
i := i + 1;
}
}
It produces
1 This loop invariant might not be maintained by the loop. 29,38
2 This loop invariant might not be maintained by the loop. 42,73
3 This loop invariant might not be maintained by the loop. 43,52
Here is a slightly modified algorithm that does verify. It shifts the elements up by doing a swap. I think with a bit more work it could be adapted to your algorithm. It just needs a slightly more complex multiset invariant (which would require a lemma about adding and removing things from multisets).
predicate sorted(a:array<int>, min:int, max:int)
requires a != null;
requires 0<= min <= max <= a.Length;
reads a;
{
forall j, k :: min <= j < k < max ==> a[j] <= a[k]
}
predicate sortedSeq(a:seq<int>)
{
forall j, k :: 0 <= j < k < |a| ==> a[j] <= a[k]
}
lemma sortedSeqSubsequenceSorted(a:seq<int>, min:int, max:int)
requires 0<= min <= max <= |a|
requires sortedSeq(a)
ensures sortedSeq(a[min .. max])
{ }
method swap(a: array<int>, i:int, j:int)
modifies a;
requires a != null && 0 <= i < j < a.Length
requires i + 1 == j
ensures a[..i] == old(a[..i])
ensures a[j+1..] == old(a[j+1..])
ensures a[j] == old(a[i])
ensures a[i] == old(a[j])
ensures multiset(a[..]) == multiset(old(a[..]))
{
var tmp := a[i];
a[i] := a[j];
a[j] := tmp;
}
method insertionSort(a: array<int>)
modifies a;
requires a != null;
requires a.Length > 0;
ensures sorted(a, 0, a.Length);
ensures multiset(a[..]) == multiset(old(a[..]));
{
var i := 0;
while(i < a.Length)
invariant 0 <= i <= a.Length
invariant sorted(a, 0, i)
invariant multiset(old(a[..])) == multiset(a[..]);
{
var key := a[i];
var j := i - 1;
ghost var a' := a[..];
assert sortedSeq(a'[0..i]);
while(j >= 0 && key < a[j])
invariant -1 <= j <= i - 1
invariant a[0 .. j+1] == a'[0 .. j+1]
invariant sorted(a, 0, j+1);
invariant a[j+1] == key == a'[i];
invariant a[j+2 .. i+1] == a'[j+1 .. i]
invariant sorted(a, j+2, i+1);
invariant multiset(old(a[..])) == multiset(a[..])
invariant forall k :: j+1 < k <= i ==> key < a[k]
{
ghost var a'' := a[..];
swap(a, j, j+1);
assert a[0..j] == a''[0..j];
assert a[0..j] == a'[0..j];
assert a[j] == a''[j+1] == a'[i] == key;
assert a[j+2..] == a''[j+2..];
assert a[j+2..i+1] == a''[j+2..i+1] == a'[j+1..i];
j := j - 1;
sortedSeqSubsequenceSorted(a'[0..i], j+1, i);
assert sortedSeq(a'[j+1..i]);
assert a[j+2 .. i+1] == a'[j+1 .. i];
assert sortedSeq(a[j+2..i+1]);
}
i := i + 1;
}
}