dafny реализация insertionsort

Question

Я новичок в Dafny, и у меня проблемы с проверкой моей вставки. Dafny говорит, что мультисети-инварианты не удерживаются, что-то еще работает нормально. После часа поиска ошибки мне понадобится помощь :) Было бы неплохо, если бы кто-нибудь мог сказать мне трюк!

Мой код:

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

Answer 1

Вот немного модифицированный алгоритм, который делает проверить. Он сдвигает элементы вверх, выполняя обмен. Я думаю, что с немного большей работой он может быть адаптирован к вашему алгоритму. Он просто нуждается в несколько более сложном мультимножеством инварианте (для чего потребуется лемма о добавлении и удалении вещей из мультимножеств).

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; 
    } 
} 

http://rise4fun.com/Dafny/Gplux