时间戳

首页 > 解决方案 > 使用 frama-c 的递归快速排序的正式证明

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

问题描述

作为家庭作业，我决定尝试使用带有 wp 和 rte 插件的 frama-c验证快速排序的实现（从此处获取并改编）。请注意，首先最左边是 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 不支持递归，因此decreases运行时忽略语句Frama-c -wp -wp-rte。

这是 gui 中的结果： 在此处输入图像描述

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

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

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

谢谢

标签： sortingquicksortframa-cformal-verificationproof-of-correctness

解决方案

首先，与 Eva 不同，WP 对递归函数没有真正的问题，除了证明终止，这是完全正交的，以证明每次函数返回时后置条件都成立（这意味着我们不必为非-终止案例）：在文献中，当您还可以证明函数始终终止时，这被称为部分正确性与完全正确性。该decreases子句仅用于证明终止，因此如果您想要完全正确，它不受支持的事实只是一个问题。对于部分正确性，一切都很好。

即为了部分正确性，递归调用被视为与任何其他调用一样：您获取被调用者的合同，证明前置条件在这一点上成立，并尝试证明调用者的后置条件，假设后置-通话后，被叫方的状态保持不变。递归调用实际上对开发人员来说更容易：由于调用者和被调用者是相同的，因此您只需编写一份合约。

现在关于失败的证明义务：当循环不变量的“已建立”部分失败时，开始调查它通常是一个好主意。这通常是比保存更简单的证明义务：对于已建立的部分，您要证明第一次遇到循环时注释成立（即这是基本情况），而对于保存，您必须证明如果您在任意循环步骤开始时假设不变量为真，则它在所述步骤结束时保持为真（即这是归纳情况）。特别是，您不能从您的先决条件中推断出right_most+1 <= INT_MAX. 也就是说，如果你有rightmost == INT_MAX，你会遇到问题，尤其是 finali++会溢出。为了避免这种算术上的细微差别，使用起来可能更简单size_tforleftmost和 to 考虑rightmost是过去要考虑的最大偏移量之一。但是，如果您要求leftmost和rightmost都严格小于INT_MAX，那么您将能够继续。

然而，这还不是全部。首先，边界计数器的不变量太弱了。你想要那个counter<=i，而不仅仅是那个counter<=rightmost。最后，有必要保护递归调用，以避免违反先决条件，leftmost或者rightmost在枢轴选择不当并且您的原始索引接近极限的情况下（即counter最终是0或1因为枢轴太小或INT_MAX因为它太大了。无论如何，只有在对应的一侧为空时才会发生这种情况）。

最后，WP（Frama-C 20.0 Calcium，使用-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
    }

推荐阅读