Is the invariant correct?

Question

I want to show that Insetion Sort is stable... Do I have to do that using an invariant??

Is the invariant the following??

At the beginning of each iteration of the for loop, if $A[a]=A[b], a<b \leq j-1$, then $A[a]$ originally appeared before $A[b]$.

Initialization: We have to show that the invariant holds before the first iteration of the loop where $j=2$. In this case, the subarray $A[1 \dots j-1]$ consists of only the element $A[1]$, so there are no $a<b \leq j-1=1$. So, the invariant holds trivially.

Maintenance: We have to check if the property maintains at each iteration. The body of the outer for loop shifts the elements $A[j-1], A[j-2], A[j-3], \dots$ one position to the right until the right position for $A[j]$ is found, at which the value of $A[j]$ will be inserted, but it doesn't change their order. So, if the invariant holds before an iteration of the loop, it still holds before the next iteration.

Termination: We have to check what happens when the loop stops. The outer for loop stops when $j=n+1$. Setting $j=n+1$ at the invariant loop, we have that for each $A[a]=A[b], a<b \leq n$, it implies that $A[a]$ appears before $A[b]$ at the initial subarray. But the subarray $A[1 \dots n]$ is the whole array. So, Insertion Sort is stable.

Is this correct?? Could I improve something??

Answer 1

If it's not required to use an invariant/induction (I'm not English native, is it what we call "récurrence" in French, where we have to prove S(n+1) given S(n)?)

So for Insertion Sort, I believe the pseudo-code says it all:

 for i = 1 to length(A) - 1
    x = A[i]
    j = i
    while j > 0 and A[j-1] > x
        A[j] = A[j-1]
        j = j - 1
    A[j] = x

For a given i, if several items already classified are equals to the one inserted x(=A[i]), then the condition A[j-1] > x imposes than we won't insert x before any of the items it is equal to, since it will fail to meet that condition then, x will be equal to A[j-1] and we will put x just in front of them at position j. Hence the stability of this sorting algorithm.