使用 frama-c 的递归快速排序的正式证明

Formal proof of a recursive Quicksort using frama-c

作为作业,我决定尝试使用带有 wp 和 rte 插件的 frama-c 来验证快速排序的实现(取自 here)。请注意,最左边的值为 0,最右边的值为 size-1。这是我的证明。

     /*@
    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
    }

作为旁注,我知道 wp 不支持递归,因此在 运行 Frama-c -wp -wp-rte.

时忽略了 decreases 语句

这是 gui 中的结果:

如您所见,我的循环不变量没有经过验证,尽管它对我来说很有意义。

Frama-c 在不支持递归的情况下能够在假设下验证第二个递归调用。据我了解,调用 quickSort(t, leftmost, counter-2) 未经过验证,因为可能违反先决条件 requires 0 <= rightmost。不过,我不太确定 Frama-c 在这种情况下的行为以及如何解决它。

我想了解正在发生的事情。我认为不变量没有被验证与递归无关,因为即使通过删除递归调用,它们也没有被验证。最后,您能否向我解释一下在递归调用的情况下 Frama-c 的行为是什么?它们是否被视为任何其他函数调用或是否存在我不知道的行为?

谢谢

首先,与 Eva 不同,WP 在递归函数方面没有真正的问题,除了证明终止完全正交以证明 post-条件成立 每次函数 returns(意味着我们不需要为非终止情况证明任何东西):在文献中,这被称为部分正确性 vs .完全正确当你还可以证明函数总是终止的时候。 decreases 子句仅用于证明终止,因此如果您想要完全正确,它不受支持的事实只是一个问题。对于部分正确性,一切都很好。

即为了部分正确性,递归调用与任何其他调用一样对待:您获取被调用者的合同,证明此时前提条件成立,并尝试证明 post-调用者的条件假设被调用者的 post 条件在调用后成立。递归调用实际上对开发者来说更​​容易:因为调用者和被调用者是相同的,你只需要写一个合约。

现在关于失败的证明义务:当循环不变量的 'established' 部分失败时,开始调查它通常是个好主意。这通常是比保存更简单的证明义务:对于已建立的部分,你想证明注释在你第一次遇到循环时成立(即这是基本情况),而对于保存,你必须证明如果您在任意循环步骤开始时假设不变量为真,则它在所述步骤结束时保持为真(即这是归纳情况)。特别是,您不能从前提条件中推断出 right_most+1 <= INT_MAX。也就是说,如果你有 rightmost == INT_MAX,你会遇到问题,尤其是最后的 i++ 会溢出。为了避免这种算术上的微妙之处,使用 size_t 代替 leftmost 并将 rightmost 视为超过要考虑的最大偏移量可能更简单。但是,如果您要求 leftmostrightmost 都严格小于 INT_MAX,那么您将能够继续。

然而,这还不是全部。首先,边界计数器的不变量太弱。您想要 counter<=i,而不仅仅是 counter<=rightmost。最后,有必要保护递归调用以避免违反 leftmostrightmost 的先决条件,以防枢轴选择不当并且您的原始索引接近极限(即 counter 最终成为 01 因为枢轴太小或 INT_MAX 因为它太大。无论如何,这只有在相应的边为空时才会发生).

最后,以下代码得到了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
    }