Apr 17, 2011 at 5:54 PM
Edited Apr 17, 2011 at 6:24 PM

Hi,
Playing with spec#, I am trying to verify my quicksort algorithm. I think the partitioning algorithm is correct (boogie agrees), but the recursive part of quicksort is not verified. The postcondition seems to be invalid, can somebody help me with this? Thanks
in advance.
static void quicksort(int[]! a, int p, int q)
requires (p >= 0 && q < a.Length && p <= q)  ( p >= q );
ensures forall { n in ( p..q ), x in ( 0..n ); a[x] <= a[n] };
modifies a[*];
{
if ( q > p )
{
int pivot = partition(a, p, q);
assert forall { n in ( p..pivot); a[n] <= a[pivot] } && forall { n in ( pivot+1..q ); a[n] > a[pivot] };
quicksort(a, p, pivot1);
quicksort(a, pivot+1, q);
}
}
static int partition(int[]! a, int p, int q)
requires p >= 0 && q < a.Length && p <= q;
ensures forall { n in ( p..result); a[n] <= a[result] };
ensures forall { n in ( result+1..q ); a[n] > a[result] };
ensures result >= p && result <= q;
modifies a[*];
{
int pivot = a[p];
int i = 0;
int k = p;
a[p] = a[q];
a[q] = pivot;
for ( i = p; i < q; i++ )
invariant forall { n in (p:k); a[n] <= pivot };
invariant forall { n in (k:i); a[n] > pivot };
invariant i >= p;
invariant i <= q;
invariant k >= p && k <= i;
{
if ( a[i] <= pivot )
{
int tmp = a[k];
a[k++] = a[i];
a[i] = tmp;
}
}
a[q] = a[k];
a[k] = pivot;
return k;
}


Developer
Apr 17, 2011 at 7:44 PM

Hi,
I have to quick remarks that might help you.
First, intervals in Spec# are halfopen. So I guess in the first postcondition of partition, you want to say:
ensures forall { n in ( p..result + 1); a[n] <= a[result] };
Otherwise, the value of a[result] is unspecified.
Second, quicksort is a bit tricky to verify because it is not sufficient to specify that the array segment after the method call is sorted; one also needs to specify the range of values of the segment. Consider the input a={1,0}, p=0, q=1. After the call
to partition, we have a={0,1} and pivot=0 or pivot=1. But now the recursive calls to quicksort might actually change a to something like {200,5} because they only guarantee that the segment they work on will be sorted. This is the case here, because {200}
is sorted and {5} is sorted, but of course {200,5} is not. So the verifier needs to know that the minimum and maximum of the segments are preserved such that it can conclude that the maximum of the left segment is less or equal to the minimum of the right
segment.
Hope this helps,
Peter



Hi Peter,
Thanks for your quick reply. I believe the interval (p..result) also includes result, while (p:result) does not. Your point about the method possibly changing the array makes sense, thanks. The proper way of dealing with this is to ensure that the resulting
segment is a permutation of the input segment, correct? I'm having some issues properly formulating an expression that checks this. The old() method does not seem to work on individual array elements, do you have any ideas on how I can fix this without resorting
to allocating new arrays?


Coordinator
Apr 17, 2011 at 8:10 PM

Furthermore, the range of x in the postcondition of quicksort should start at p, not 0.
Also, you need to say, for both quicksort and partition, that the array elements outside the range p..q are not modified. To prove that for partition, the loop invariant of partition needs to say that those array elements are unmodified.
That's tricky to do in Spec#, because Spec# does not allow you to use "old" expressions in loop invariants.
By the way, it's a bit unfortunate that the precondition of quicksort has that disjunction. You can eliminate it in various ways. For example, I would have started by letting p,q denote a halfopen interval of array indices, in which case your
quicksort precondition would be simply: 0 <= p && p <= q && q <= a.Length. (Note also that by writing all arithmetic inequalities like < or <=, as opposed to a mix of those and > and >=, you can directly "see"
from the formula that p lies between 0 and q and that q lies between p and a.Length, which is not as easy to detect when the inequalities are written in an arbitrary order.)
Best wishes,
Rustan


Coordinator
Apr 17, 2011 at 8:15 PM

"old" does work on array elements. For example, old(a[i]) refers to the value of a[i] in the prestate. However, you cannot in Spec# use "old" in loop invariants. To work around that is somewhat of a pain. As one of those possible
but painful ways is to recode "partition" using recursion instead of the loop.
To specify that the output is a permutation of the input would indeed be the most complete specification. One way to do that is for you to construct the partition as you go along in another array. (I think there may be some Dafny example in boogie.codeplex.com
under the Test folder that does that, but perhaps I'm misremembering.) Something awkward with that is that Spec# does not support ghost variables and ghost arrays.



Thanks for your feedback. Are there any plans on supporting old() inside loop invariants? By the way, I appreciate your videos on channel9. Do you plan on creating more?


Apr 18, 2011 at 9:38 AM
Edited Apr 18, 2011 at 9:40 AM

One other issue, when I try to use old(a[x]) inside a comprehension, it fails. It will yield either 'use of unassigned variable x' or 'internal error: name resolution errors detected'. For example:
product { int x in (p..q); old(a[x]) } == 1;

