如何用递归证明插入排序的正确性？

Question

我必须使用递归进行插入排序，并通过使用循环不变量来证明其正确性。我相信我的代码是正确的，并且它适用于不同的输入。但是，我不知道如何像我的书那样证明它的正确性。有人可以通过使用循环不变量来证明它是正确的吗？

通过使用以下类似于数学归纳的步骤，在书中证明了这些算法是正确的。如有需要，请参考enter link description here

1 - 找到算法中每个循环的循环不变量。循环不变量是在循环开始之前、任何后续迭代之后以及循环终止时为真的条件。

2 - 使用逻辑证明循环不变量在循环初始化之前为真，在后续循环运行中维护，并且在循环具有时为真终止。

//n - The index till which the array D is to be sorted.
public static void sort(int n, int [] D){
    if(n == 0){
        return;
    }else {
        sort(n-1, D);
    }

    int lastItem = D[n];
    int j = n-1;

    while (j >= 0 && lastItem < D[j]) {
        D[j + 1] = D[j];
        j--;
    }

    //Insert the lastItem at the correct position.
    D[j+1] = lastItem;
}

}

PS - 我使用的书是 Thomas Cormen 的“算法简介”，即 CLRS 书。

Answer 1

循环不变式是在调用D[0..n] 之后包含原始数组的第一个n 值以及所有i < n、D[i] <= D[i+1]。

对于n = 0 来说，这是微不足道的。在递归调用之后，您通过归纳知道n-1 是正确的。 “包含原始数组的第一个 n 值”is true at all points. The conditionD[i]

祝你正式写出来很开心！ :-)

Answer 2

可能是答案有些多余。 为方便起见，我们将方法分为两部分 - 递归和循环。循环不变量在下面的代码中描述：

// Correctness of sort can be proved by mathematical induction
public static void sort(int n, int[] D)
{
    if (n == 0)
    {
        return;
    }
    else
    {
        sort(n - 1, D);
    }
    InsertNElementInSortedArray(n, D);
}

// This method insert n-th element of D in already sorted slice D[0 .. n-1] (right bound included).
// After method execution we have sorted slice D[0 .. n] (right bound included).
// Case 1. n==0. We swap 0-th element with 0-th element.
// Case 2. n > 0 and first n element sorted in D. Use loop invariant method only for this case.
// P.S. Case 1-2 can be combined.
public static void InsertNElementInSortedArray(int n, int[] D)
{
    int lastItem = D[n];
    int j = n - 1;

    // Define DR as slice of D[j+1 .. n] (right bound included)
    // Define DL as slice of D[0 .. j] (right bound included)
    // Loop invariant: DR are sorted
    //                 DL are sorted 
    //                 All elements in DR except first element are greater or equal than all elements in DL
    //                 All elements in DR except first element are greater or equal than lastItem
    //                 DR (except first element) and DL contains all elements from source D[0 .. n-1] (right bound included)
    //
    // Initialization: It is true prior to the first iteration of the loop:
    //                 DR are sorted because DR have only one element
    //                 DL are sorted because first n element sorted in D
    //                 All elements in DR except first are greater or equal than all elements in DL because DR have only one element lastItem
    //                 All elements in DR except first element are greater or equal than lastItem because DR have only one element lastItem
    //                 DR(except first element) and DL contains all elements from source D[0..n - 1] because DL == D[0..n - 1]
    //
    // Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration because
    //              In loop step we take last element from DL and replace them first element in DR and next change boundaries of DL and DR.
    //              DR are sorted because all elements in DR except first element are greater or equal than all elements in DL
    //              DL are sorted because first n element sorted in source D
    //              All elements in DR except first element are greater or equal than all elements in DL because we take maximum element from DL 
    //              All elements in DR except first element are greater or equal than lastItem because lastItem less than maximum element from DL (by loop condition)
    //              DR (except first element) and DL contains all elements from source D[0 .. n-1] by construction
    while (j >= 0 && lastItem < D[j])
    {
        D[j + 1] = D[j];
        j--;
    }

    // Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.
    //              When loop terminates we have
    //              DR sorted
    //              DL sorted
    //              All elements in DR except first element are greater or equal than all elements in DL
    //              All elements in DR except first element are greater or equal than lastItem
    //              DR (except first element) and DL contains all elements from source D[0 .. n-1] (right bound included)
    //              
    //              1 case. Loop terminates when lastItem >= D[j].
    //                      lastItem is greater or equal than all elements in DL.
    //                      Replace first element from DR by lastItem. Now we have DR >= DL and both slices sorted then D[0 .. n] sorted.
    //              
    //              2 case. Loop terminates when j == -1.
    //                      DR contains all elements from source D[0 .. n-1] and DR sorted.
    //                      lastItem is less than all elements from DR.
    //                      When we assign D[0] = lastItem then then D[0 .. n] sorted.
    D[j + 1] = lastItem;
}