插入排序的 dafny 实现

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