InsertSort invariant

Feb 26, 2014 at 3:23 PM
Edited Feb 26, 2014 at 3:25 PM
Hello,
I'm trying to verify the InsertSort you can find below. But Dafny said that the last inner invariant
  invariant sorted(a,j,i);
is not maintained by the loop, however the two asserts
            assert a[j-1] <= a[j];
            assert (sorted(a,j,i) && a[j-1] <= a[j]) ==> sorted(a,j-1,i);
are admitted.
Paqui
predicate sorted(a : array<int>, i : int, j : int)
requires a!=null;
reads a;
requires 0 <= i < a.Length && 0 <= j < a.Length;
{
  forall x, y :: i <= x < y <= j ==> a[x] <= a[y]
}

method insertSort(a : array<int>)  
    modifies a;  
    requires a != null && a.Length > 0;    
    ensures sorted(a,0,a.Length-1);  
{  
    var i := 1;    
    while (i < a.Length)  
        invariant 0 < i <= a.Length;           
        invariant sorted(a,0,i-1); 
        {  
        var j := i;  

        while (j > 0 && a[j-1] > a[j])  
            invariant 0 <= j <= i <= a.Length;      
            invariant j > 0 ==> sorted(a,0,j-1);   
            invariant sorted(a,j,i);
            {  

            a[j], a[j-1] := a[j-1], a[j]; 

            assert a[j-1] <= a[j];
            assert (sorted(a,j,i) && a[j-1] <= a[j]) ==> sorted(a,j-1,i);

            j := j - 1;  
            }  
        assert sorted(a,0,i);
        i := i + 1;  
        }  
}  
Coordinator
Feb 27, 2014 at 6:55 PM
Hi Paqui,

The inner loop invariant is not strong enough. Dafny considers a case like this:
Value of array a:
index:  0 1 2 3 ... j-1 j j+1 j+2 ... a.Length-1
value:  8 8 8 8 ...  8  5  2   2  ...     2
        +------------+     +--------------+
        sorted(a,0,j-1)    sorted(a,j,i)
Note that the loop invariant for your inner loop holds for this example. In particular, the subarray before index j and the subarrays after index j are both sorted, as indicated in my ASCII diagram above. You also need the information that everything in the lower subarray is less than everything in the upper subarray, which you can express by:
a[j-1] <= a[j+1]
when j-1 and j+1 are array indices not exceeding I.

By the way, I have two suggestions for the predicate sorted. One suggestion is to let the "i" and "j" parameters of sorted be a half-open interval rather than a closed interval. In other words, let "j" be just above all the array indices you want to compare. The other suggestion is to tighten up the precondition to require "i" and "j" never to specify a "negative" range (empty range is fine, but not a "negative" range). For example, don't allow anyone to call sorted(a, 10, 3). Sometimes it is convenient to allow as many parameter values as possible, but whenever you can, it's better to give a stronger precondition, because then Dafny will detect any unintentional parameter values at the call site (avoiding the situation where you may accidentally have given bad parameter values at a call site and this leaves you confused about why something is not verifying). Following my own two suggestions, here's how I would have defined sorted:
predicate sorted(a : array<int>, i : int, j : int)
  requires a!=null;
  reads a;
  requires 0 <= i <= j <= a.Length;
{
  forall x, y :: i <= x < y < j ==> a[x] <= a[y]
}
Rustan
Marked as answer by rustanleino on 2/27/2014 at 11:56 AM
Mar 3, 2014 at 9:37 AM
Hi Rustan,
Thanks for your suggestions on predicate sorted, I'll take them into account in new versions,
but, by now, let me insist on the same program.
I'm sorry but I don't understand the above counter-example:
Value of array a:
index:  0 1 2 3 ... j-1 j j+1 j+2 ... a.Length-1
value:  8 8 8 8 ...  8  5  2   2  ...     2
        +------------+     +--------------+
        sorted(a,0,j-1)    sorted(a,j,i)
since you have represented sorted(a,j,i) like sorted(a,j+1,i).
Actually, the 5 in a[j] makes that my invariant does not hold.
Anyway, probably I didn't explain well my exact question.
What is very strange for me is that Dafny says that the invariant:
 invariant sorted(a,j,i);
might not be maintained by the loop, while the assertions
(in my previous version "<" was "<=", I have corrected, but this does not affect what I'm commenting now):
assert a[j-1] < a[j];
assert (sorted(a,j,i) && a[j-1] < a[j]) ==> sorted(a,j-1,i);
are perfectly verified after the double assignment
a[j], a[j-1] := a[j-1], a[j]; 
To my knowledge, these two assertions are the crucial ones to prove the preservation of
the above invariant, so I can not understand why Dafny is not able to prove that invariant preservation property.
Best,
Paqui
May 12, 2014 at 2:40 PM
Edited May 12, 2014 at 2:41 PM
Hi Rustan,
I had forgotten to tell you that I had solved this problem.
I think my solution is a beautiful program for teaching.
Here you are.
Paqui
predicate sorted(a : array<int>, i : int, j : int)
  requires a!=null;
  reads a;
  requires 0 <= i <= j <= a.Length;
{
  forall x, y :: i <= x < y < j ==> a[x] <= a[y]
}

method insertSort(a : array<int>)  
    modifies a;  
    requires a != null && a.Length > 0;    
    ensures sorted(a,0,a.Length);  
{  
    var i := 1;    
    while (i < a.Length)  
        invariant 1 <= i <= a.Length;           
        invariant sorted(a,0,i); 
        {  
        var j := i;  
        while (j > 0 && a[j-1] > a[j])  
            invariant 0 <= j <= i < a.Length;      
            invariant sorted(a,0,j);    
            invariant sorted(a,j,i+1);
            invariant forall x,y :: (0 <= x < j && j+1 <= y <= i) ==> a[x] <= a[y];
            {  
            a[j], a[j-1] := a[j-1], a[j]; 
                // assert sorted(a,0,j-1) && sorted(a,j,i+1) && j > 0 && a[j-1] < a[j];
            j := j - 1;  
            }  
        i := i + 1;  
        }  
}