CODEWITHSUNDEEP
sortinginsertion-sortdafny
jnk
jnk

Reputation: 5

dafny implementation of insertionsort

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

Link: http://rise4fun.com/Dafny/3R5

Upvotes: 0

Views: 2543

Answers (2)

Peter Gumm
Peter Gumm

Reputation: 11

Using parallel assignment instead of calling swap, there is a simpler solution:

ghost predicate sorted(a:seq<int>)
{∀ i,j | 0 ≤  i < j  < |a| :: a[i] ≤ a[j] }

method InsertionSort(a:array<int>)
  modifies a
  requires a.Length ≥ 2
  ensures sorted(a[..])
  ensures multiset(a[..]) == multiset(old(a[..]))
{
  var x := 1;
  while x < a.Length
    invariant 1 ≤ x ≤ a.Length;
    invariant sorted(a[..x]);
    invariant multiset(a[..]) == multiset(old(a[..]))
  {
    var d := x;
    while d >= 1 && a[d-1] > a[d]
      invariant 0 ≤ d ≤ x;
      invariant ∀ i,j |( 0 ≤ i < j ≤ x && j ≠ d) :: a[i] ≤ a[j]
      invariant multiset(a[..]) == multiset(old(a[..]))
    {
      a[d-1],a[d] := a[d], a[d-1];
      d := d-1;
    }
    x := x+1;
  }
}

Upvotes: 1

lexicalscope
lexicalscope

Reputation: 7328

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

http://rise4fun.com/Dafny/Gplux

Upvotes: 1

Related Questions