Я новичок в Dafny, и у меня проблемы с проверкой моей реализации InsertSort. Дафни говорит мне, что инварианты мультимножества не выполняются, все остальное работает нормально. После нескольких часов поиска ошибки мне может понадобиться помощь :) Было бы неплохо, если бы кто-нибудь мог сказать мне трюк!
Мой код:
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;
}
}
Он производит
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
Ссылка: http://rise4fun.com/Dafny/3R5