Rigorous Proof of Insertion Sort

Question

Currently I self study CLRS book (Outside of any course, so I got no access to an instructor)

And I am stuck proving Insertion Sort, The proof in CLRS book is not so formal.

Here's the algorithm:

INSERTION-SORT(A)
   for j=2 to A.length (= n)
      key = A[j]
      i = j-1
      while (0<i and key<A[i])
         A[i+1]=A[i]
         i = i-1
      end while
      A[i+1]=key
   end for
end procedure

I tried to formalize the proof with the following pre-post conditions:

Pre-Condition: $A=A_{org}$ and $j=2$ (I.e. $A_{org}$ holds the original values of $A$)
Post-Condition: The array $A$ consists of the same elements as in $A_{org}$ but in a sorted order that is $\forall i_1,i_2\in\{1..n\}, i_1<i_2\to A[i_1]\leq A[i_2]$.

My loop invariant is:
($p$ denotes the $p$'s iteration)

$I(p)="\text{The array $A[1..j-1]$ consists of the same elements as in $A_{org}[1..j-1]$} \land \forall i_1,i_2\in\{1..j-1\}, i_1<i_2\to A[i_1]\leq A[i_2] \land j=2+p"$

Now when I try to prove the inductive step I got stuck and cannot proceed because of the nested $while$ loop and because of the informal sentence "The array $A[1..j-1]$ consists of the same elements as in $A_{org}[1..j-1]$".

Any help on how to prove Insertion Sort rigorously and how to formalize the sentence "The array $A[1..j-1]$ consists of the same elements as in $A_{org}[1..j-1]$" will be appreciated (I want my loop invariant to contain only mathematical symbols and not informal english phrases).

(BTW: I am trying to write the proof in the same style as in Susanna. Epp's Discrete Mathematics book)

Any help will be appreciated. Thanks.

Answer 1

Hint: first prove a loop invariant for the nested while, i.e. you need to prove that the nested while shifts to the right the elements as required to insert the j-element indexed by the outer for loop in its correct place. Then, prove the loop invariant for the outer for loop taking into account the suggestion by @Yuval and you are done.

Answer 2

The formal statement of "$A[1\ldots j-1]$ consists of the same elements as $A_{\mathrm{org}}[1\ldots j-1]$" is "there exists a permutation $\pi\colon \{1,\ldots,j-1\}\to\{1,\ldots,j-1\}$ such that $A[i] = A_{\mathrm{org}}[\pi(i)]$". Formal statements are in English unless you're doing formal logic.

Your induction hypothesis isn't strong enough. It only tells you something about the first $j-1$ elements in both arrays, whereas in the next step you'll have to talk about $j$ elements of both arrays. You need to mention that elements $j$ to $n$ are the same in both arrays.

Regarding formal proof, it really depends how formal you want to be. If you have a formal logic in mind for proving the correctness of programs, then you can attempts to give a formal proof. Such a system might require preconditions and postconditions for each statement; in fact, you'll need to do something for any subexpression. I'm assuming you're not going that far, however, and in that case the notion of "formal proof" depends on your level of experience and your target audience. If you're self-studying, your target audience is yourself, so you need a proof that you find convincing. It's much preferable if somebody else (an expert, say a graduate student) went over your proof, since it's hard to understand the common standard otherwise.

Another relevant question is why you're interested in a "formal" proof. Unless you're going into software verification, there's probably no need for a formal proof, but rather for a convincing proof. What convinces you depends on your level and experience, but I often find that overly formal proofs are harder to understand. But it's up to you, and perhaps it's useful to go formal at least once in your studies. For the algorithms practitioner – algorithm developer or algorithm implementer – there is usually no need for such a formal level of detail.

Answer 3

There is actually a simpler way to prove this. This is a quite simple algorithm. I think a good English explanation is rigorous enough.

• There is an invariant within each outer loop body. The invariant is: for all pairs of two numbers, such that none of the two number is currently the one used as key on line 3, then the order of the pair does not change before and after the completion of the current iteration of the main outer loop. [1]
• All numbers are preserved. If they are in the original array, they will still be in the output. [2]

Now assume the output array is not sorted, there exists at least one pair of numbers with incorrect order. We will pick the pair which has the largest difference, say $<a_i, a_j>$. At some point, $a_j$ must be used as key in line 3 because every number in the array will be picked as key. Now, the inner loop completes when it finds another number $a_i'$ such that $a_i'$ < $a_j$ or it completes when it finds $a_i$.

If the inner loops find $a_i$, then it will change the order of the pair $<a_i, a_j>$ and this order will stay the same until the process completes which gives us a contradiction about the order of this pair.

If the inner loop finds another $a_i'$ such that $a_i' <a_j$, then this pair's order will stay the same when the process completes also because of [1]. Then the mis-ordered pair with the largest difference is not $<a_i, a_j>$, but this pair instead. This is a contradiction

You can try to translate this into formal logic too, but it will be quite tiring. Maybe it is a good practice for you.