使用frama-c的递归Quicksort的形式证明

Question

[作为作业，我决定尝试使用带有wp和rte插件的frama-c来验证quicksort的实现（取自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不支持递归，因此在运行decreases时忽略了Frama-c -wp -wp-rte语句。

这是gui中的结果：

您可以看到我的循环不变量即使对我来说也没有经过验证。

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

我想了解发生了什么。我认为不验证不变量与递归无关，即使通过删除递归调用也不会对其进行验证。最后，您能否向我解释在递归调用的情况下Frama-c的行为是什么？是否将它们视为其他任何函数调用，还是我不知道的行为？

谢谢

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-C 20.0钙，使用-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
    }