Formal proof of a recursive Quicksort using frama-c

Question

As homework, I've decided to try verify an implementation of quicksort (taken and adapted from here) using frama-c with wp and rte plugins. Note that at first leftmost is 0 and rightmost is equal to size-1. Here my proof.

     /*@
    requires \valid(a);
    requires \valid(b);
    ensures *a == \old(*b);
    ensures *b == \old(*a);
    assigns *a,*b;
    */
    void swap(int *a, int *b)
    {
        int temp = *a;
        *a = *b;
        *b = temp;
    }

    /*@
    requires \valid(t +(leftmost..rightmost));
    requires 0 <= leftmost;
    requires 0 <= rightmost;
    decreases (rightmost - leftmost);
    assigns *(t+(leftmost..rightmost));
    */
    void quickSort(int * t, int leftmost, int rightmost)
    {
        // Base case: No need to sort arrays of length <= 1
        if (leftmost >= rightmost)
        {
            return;
        }  // Index indicating the "split" between elements smaller than pivot and 
        // elements greater than pivot
        int pivot = t[rightmost];
        int counter = leftmost;
        /*@
            loop assigns i, counter, *(t+(leftmost..rightmost));
            loop invariant 0 <= leftmost <= i <= rightmost + 1 <= INT_MAX ;
            loop invariant 0 <= leftmost <= counter <= rightmost;
            loop invariant \forall int i; leftmost <= i < counter ==> t[i] <= pivot;
            loop variant rightmost - i;
        */
        for (int i = leftmost; i <= rightmost; i++)
        {
            if (t[i] <= pivot)
            {
                /*@assert \valid(&t[counter]);*/
                /*@assert \valid(&t[i]);*/
                swap(&t[counter], &t[i]);
                counter++;
            }
        }

        // NOTE: counter is currently at one plus the pivot's index 
        // (Hence, the counter-2 when recursively sorting the left side of pivot)
        quickSort(t, leftmost, counter-2); // Recursively sort the left side of pivot
        quickSort(t, counter, rightmost);   // Recursively sort the right side of pivot
    }

As side note, I know that wp doesn't support recursion hence the ignored decreases statement when running Frama-c -wp -wp-rte.

here is the result in the gui:

As you can see my loop invariants are not verified even though it makes senses to me.

Frama-c able to verify under hypotheses the second recursive call when it's not supporting recursion. To my understanding the call quickSort(t, leftmost, counter-2) isn't verified since can violate the precondition requires 0 <= rightmost. I'am not too sure about Frama-c behaviour in that case though and how to tackle it.

I would like some input about what is going on. I think that the invariant not being verified as nothing to do with recursion as even by removing the recursion calls, they aren't verified. And finally could you explain to me what is the Frama-c behaviour in the case of the recursive calls? Are they treated as any other function call or is there a behaviour that I'am unaware of?

Thanks

Answer 1

First, unlike Eva, WP has no real problem with recursive functions, apart from proving termination, which is completely orthogonal to prove that the post-condition holds each time the function returns (meaning that we don't have to prove anything for the non-terminating cases): in the literature, this is referred to as partial correctness vs. total correctness when you can also prove that the function always terminates. The decreases clause only serves to prove termination, so that the fact that it is unsupported is only an issue if you want total correctness. For partial correctness, everything is fine.

Namely for partial correctness, a recursive call is treated like any other call: you take the contract of the callee, prove that the pre-condition holds at this point, and try to prove the post-condition of the caller assuming that the post-condition of the callee holds after the call. Recursive calls are in fact easier for the developer: since the caller and the callee are the same, you get to write only one contract 😛.

Now regarding the proof obligations that fail: when the 'established' part of a loop invariant fails, it is often a good idea to start investigating that. This is usually a simpler proof obligation than the preservation: for the established part, you want to prove that the annotation holds when you encounter the loop the first time (i.e. this is the base case), while for the preservation, you have to prove that if you assume the invariant true at the beginning of an arbitrary loop step, it stays true at the end of said step (i.e. this is the inductive case). In particular, you can not deduce from your pre-conditions that right_most+1 <= INT_MAX. Namely, if you have rightmost == INT_MAX, you will encounter issues, especially as the final i++ will overflow. In order to avoid such arithmetic subtleties, it is probably simpler to use size_t for leftmost and to consider rightmost to be one past the greatest offset to consider. However, if you requires that both leftmost and rightmost to be strictly less than INT_MAX, then you will be able to proceed.

However, that is not all. First, your invariant for bounding counter is too weak. You want that counter<=i, not merely that counter<=rightmost. Finally, it is necessary to guard the recursive calls to avoid violating the pre-conditions for leftmost or rightmost in case the pivot was ill-chosen and your original indices were close to the limit (i.e. counter ends up being 0 or 1 because the pivot was too small or INT_MAX because it was too big. In any case, this can only happen if the corresponding side would be empty).

In the end, the following code gets completely proved by WP (Frama-C 20.0 Calcium, using -wp -wp-rte):

#include <limits.h>
/*@
    requires \valid(a);
    requires \valid(b);
    ensures *a == \old(*b);
    ensures *b == \old(*a);
    assigns *a,*b;
    */
    void swap(int *a, int *b)
    {
        int temp = *a;
        *a = *b;
        *b = temp;
    }

    /*@
    requires \valid(t +(leftmost..rightmost));
    requires 0 <= leftmost < INT_MAX;
    requires 0 <= rightmost < INT_MAX;
    decreases (rightmost - leftmost);
    assigns *(t+(leftmost..rightmost));
    */
    void quickSort(int * t, int leftmost, int rightmost)
    {
        // Base case: No need to sort arrays of length <= 1
        if (leftmost >= rightmost)
        {
            return;
        }  // Index indicating the "split" between elements smaller than pivot and 
        // elements greater than pivot
        int pivot = t[rightmost];
        int counter = leftmost;
        /*@
            loop assigns i, counter, *(t+(leftmost..rightmost));
            loop invariant 0 <= leftmost <= i <= rightmost + 1;
            loop invariant 0 <= leftmost <= counter <= i;
            loop invariant \forall int i; leftmost <= i < counter ==> t[i] <= pivot;
            loop variant rightmost - i;
        */
        for (int i = leftmost; i <= rightmost; i++)
        {
            if (t[i] <= pivot)
            {
                /*@assert \valid(&t[counter]);*/
                /*@assert \valid(&t[i]);*/
                swap(&t[counter], &t[i]);
                counter++;
            }
        }

        // NOTE: counter is currently at one plus the pivot's index 
        // (Hence, the counter-2 when recursively sorting the left side of pivot)
        if (counter >= 2)
        quickSort(t, leftmost, counter-2); // Recursively sort the left side of pivot
        if (counter < INT_MAX)
        quickSort(t, counter, rightmost);   // Recursively sort the right side of pivot
    }