使用frama-c对递归快速排序的形式化证明

Question

作为家庭作业，我决定尝试使用frama和wp和rte插件来验证快速排序(从这里中获取和改编)的实现。注意，首先，最左边等于0，最右边等于大小-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不支持递归，因此在运行decreases时忽略了Frama-c -wp -wp-rte语句。

这是gui中的结果：

​

正如你所看到的，我的循环不变量没有被验证，即使它对我有意义。

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

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

谢谢

Answer 1

首先，与Eva不同，WP对于递归函数没有真正的问题，除了证明终止，它是完全正交的，以证明每次函数返回时后置条件仍然有效(这意味着我们不需要为不终止的情况证明任何东西)：在文献中，这被称为部分正确性与完全正确性，当你也可以证明函数总是终止的时候。decreases子句只用于证明终止，因此它不受支持的事实只是一个问题，如果您想要完全正确的话。就部分正确性而言，一切都很好。

即，对于部分正确性，递归调用与任何其他调用一样:您接受被调用方的契约，证明前置条件在这一点上有效，并试图证明调用方的后条件假设被调用者的后条件在调用之后仍然有效。对于开发人员来说，递归调用实际上更容易:因为调用方和被调用方是相同的，所以只需要编写一个契约。

现在，关于失败的证明义务:当循环不变式的“已建立”部分失败时，开始研究它通常是个好主意。这通常是一种比保存更简单的证明义务:对于已建立的部分，您希望证明当您第一次遇到循环时(即这是基本情况)注释仍然有效，而对于保存，您必须证明如果在任意循环步骤开始时假设不变为真，则在所述步骤的末尾(即，这是归纳的情况)，它保持为真。特别是，你不能从你的前提条件推断right_most+1 <= INT_MAX.也就是说，如果您有rightmost == INT_MAX，您将遇到问题，特别是当最终的i++将溢出时。为了避免这种算法的微妙性，使用size_t进行leftmost并将rightmost视为需要考虑的最大偏移量可能更简单。但是，如果您要求leftmost和rightmost都严格小于INT_MAX，那么您就可以继续下去了。

然而，这还不是全部。首先，包围计数器的不变量太弱了。你想要那个counter<=i，而不仅仅是那个counter<=rightmost。最后，有必要保护递归调用，以避免违反leftmost或rightmost的预先条件，以防支点选择不当，并且您的原始指数接近极限(例如，由于支点太小，counter最终成为0或1，而INT_MAX则因为太大)。在任何情况下，只有当相应的侧为空时，才能发生这种情况)。

最后，WP (Frama-C20.0Ca，使用-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
    }