CODEWITHSUNDEEP
arraysintsortingformal-verificationdafny
Jesus Barba
Jesus Barba

Reputation: 29

Dafny Insert int into Sorted Array method

I'm trying to prove this program in dafny but I still get an error with the last invariant and I can't see why it's not working.

The program consists on a method which inserts an int into a sorted array. The int will be inserted in the correct position ie: inserting 5 into 1,2,3,4,5,6,7 will return: 1,2,3,4,5,5,6,7

function sorted (a: array<int>): bool
  requires a != null ;
  reads a;
  {
    forall i :: 0 <= i < (a.Length - 1) ==> a[i] <= a[ i+1]
  }

method InsertSorted(a: array<int>, key: int ) returns (b: array<int>)
  requires a != null && sorted(a);
  ensures b != null ;
  ensures sorted(b);
   {
     var i:= 0;
     b:= new int[a.Length + 1];

     if(a.Length > 0){
      while (i < a.Length)
      invariant 0<= i;
      invariant i <= a.Length;
      invariant b.Length == a.Length + 1;
      invariant sorted(a);
      invariant forall j :: 0 <= j < i ==> b[j] <= b[j+1];
      {
        if(a[i]<=key)
        {
          b[i]:= a[i];
          b [i+1] := key;
          assert b[i] <= b[i+1];         
        }
        else if (key > a[i])
        {
          if(i==0)
          {
            b[i] := key;
          }
          b [i+1] := a[i];
          assert key > a[i];
          assert b[i]<= b[i+1];
        }
        else{
          b[i]:= a[i];
          b [i+1] := a[i];
          assert sorted(a);
          assert b[i] <= b[i+1];
        }
        assert b[i]<= b[i+1];
        i := i+1;
      }
     }
     else{
       b[0] := key;
     }
   }

Thanks

Upvotes: 1

Views: 1492

Answers (1)

lexicalscope
lexicalscope

Reputation: 7328

I think that perhaps you algorithm is not correct. In any case, I find the conditionals hard to understand, if the first branch is not taken then we know that !(a[i] <= key) or more simply a[i] > key which implies that the second branch guarded by key > a[i] is unreachable.

!(a[i]<=key) && a[i] < key ==> false

In any case, I suspect the loop invariant isn't strong enough to prove even a correct version since you are not keeping track of the state of b in sufficient detail.

Below is a proof of an algorithm that is similar to yours, showing a stronger loop invariant. I keep track of where in the array key is inserted using a ghost variable (a variable that is just used for verification and will not appear in the compiler output).

http://rise4fun.com/Dafny/RqGi

predicate sorted (a: seq<int>)
{
 forall i,j :: 0 <= i < j < |a| ==> a[i] <= a[j]
}

predicate lessThan(a:seq<int>, key:int) {
 forall i :: 0 <= i < |a| ==> a[i] < key
}

predicate greaterEqualThan(a:seq<int>, key:int) {
 forall i :: 0 <= i < |a| ==> a[i] >= key
}

method InsertSorted(a: array<int>, key: int ) returns (b: array<int>)
  requires a != null && sorted(a[..])
  ensures b != null && sorted(b[..]);
{
 b:= new int[a.Length + 1];

 ghost var k := 0;
 b[0] := key;

 ghost var a' := a[..];

 var i:= 0;
 while (i < a.Length)
  modifies b;
  invariant 0 <= k <= i <= a.Length
  invariant b.Length == a.Length + 1
  invariant a[..] == a'
  invariant lessThan(a[..i], key) ==> i == k;
  invariant lessThan(a[..k], key)
  invariant b[..k] == a[..k]
  invariant b[k] == key
  invariant k < i ==> b[k+1..i+1] == a[k..i]
  invariant k < i ==> greaterEqualThan(b[k+1..i+1], key)
  invariant 0 <= k < b.Length && b[k] == key
  {
    if(a[i]<key)
    {
      b[i]:= a[i];
      b[i+1] := key;
      k := i+1;
    }
    else if (a[i] >= key)
    {
      b[i+1] := a[i];
    }
    i := i+1;
  }
  assert b[..] == a[..k] + [key] + a[k..];

}

Upvotes: 1

Related Questions