Prove correctness of algorithm using induction

Question

Bubblesort(A)
int i, j;  

for i from 1 to n 
{
    for j from n-1 downto i 
    { 
        if (A[j] > A[j+1])
            swap(A[j], A[j+1]) 
    } 
}

Could we prove the correctness of the above algorithm, using induction?

If so, could you give me some hints how we could do this?

EDIT: At the base case, we check the case $i=1$, right? $$$$

For $i=1 $ we compare pairwise the elements $ (A[n], A[n-1]) $, $(A[n-1],A[n-2]) , \dots, (A[2],A[1])$ and if $A[i]>A[i+1], i \in \{ 1, \dots, n-1 \}$ then we swap their values, right?

So what can we say for the base case?

Also, what do we have to suppose at the induction hypothesis?

Answer 1

Your algorithm has a typo. The inner loop should start $j := i + 1$ and go to $n$. Notice that after iteration $i$ of the outer loop, the largest $i$ elements are sorted correctly at the end of the list. Prove this fact, which I will call $(*)$.

We also have termination, by finiteness of both loops (and no modification of $i, j$ other than incrementation).

You can then use induction on $(*)$ to argue that if the largest elements are sorted correctly at indices $n-i, ..., n-1$, then the next iteration of the loop will correctly place the $n-1-i$ largest element at index $n - 1 - i$, preserving order.

Edit:

Claim: On the ith iteration of the outer loop, the largest $i$ elements will be sorted correctly (at the end of the array).

Proof: By induction on $n \in \mathbb{N}$. Consider the base case of $n = 1$. Let $x$ be the largest element in the array. By the algorithm, if $x$ is unique, $x$ is swapped on each iteration after being discovered initially. It is then placed at the end. If $x$ is not unique, then there exists a second copy of it and no swap will occur. However, the second copy will then be swapped. This process continues, so the last occurrence of $x$ will be moved to the end of the array. The theorem thus holds at $i = 1$.

I assume the theorem holds true up to an arbitrary integer $k$ such that $1 < k < n$ and prove true for the $k+1$ case. Let $y$ be the $k+1$ largest element in the array. We consider the reduced case of examining the first $n - k - 1$ elements. By the inductive hypothesis, $y$ will be correctly placed at the end of this sub-array. As $y$ is no bigger than the $k$th largest element, $y$ will not be moved further down into the array. The $k+1$ case thus holds.

And so the claim holds true by the principle of mathematical induction.

Answer 2

Your algorithm is correct, and so is the algorithm that ml0105 gave. But whichever algorithm you use, you will certainly need two nested inductions. I will prove your algorithm but exactly the same structure can be used to prove the other algorithm.

Firstly I would encourage you to write down the invariances embedded into the code itself as it is most natural to follow the structure of the loops rather than trying to talk about them from the outside. I have put the (post-)invariances at the end of each loop, which you have to prove to hold before the first loop and also prove to hold after each loop, and can use it at the start of each loop. Those and the rest of the proof are put into the code as comments enclosed between /* and */.

Bubblesort(array A,int n)
{
    int i,j;
    /*
    A[1..0] is sorted.
    A[1..0] are before all elements in A[1..n].
    */
    for i from 1 to n 
    {
        /*
        A[1..i-1] is sorted and before all elements in A[i..n] by Invariance.
        A[n] is before all elements in A[j+1..n].
        */
        for j from n-1 downto i 
        {
            /*
            Let t = A[j+1].
            t is before all elements in A[j+2..n] by Invariance.
            */
            if (A[j] > A[j+1]) swap(A[j],A[j+1]);
            /*
            t = A[j] or t = A[j+1].
            A[j] <= A[j+1].
            Thus A[j] <= t.
            Thus A[j] is before all elements in A[j+1..n].
            Thus Invariance is preserved.
            Invariance:
                A[j] is before all elements in A[j+1..n].
            */
        }
        /*
        Therefore A[i] is before all elements in A[i+1..n].
        Also A[1..i-1] is still sorted and before A[i] because only A[i..n] were permuted.
        Thus A[1..i] is sorted and before all elements in A[i+1..n].
        Thus Invariance is preserved.
        Invariance:
            A[1..i] is sorted and before all elements in A[i+1..n].
        */
    }
    /*
    Therefore A[1..n] is sorted.
    */
}

Here is an English version but it is inadvisable for if you want to absolutely rigorously verify anything but the most trivial algorithms, simply because it is difficult to refer precisely to the points within the execution of the code itself.

Let $P(k) = ( \text{After the loop for $i = k$: $A[1..k]$ is sorted and before all elements in A[k+1..n]} )$.

Then $P(0) = true$. [Note that "after the loop for $i = 0$" means "before the loop for $i = 1$".]

During the loop for $i$:

  $P(i-1) = true$ and hence $A[1..i-1]$ are sorted and before all elements in $A[i..n]$.

  Let $Q(m) = ( \text{ After the loop for $j = m$: $A[m]$ is before all elements in $A[m+1..n]$} )$.

  Then $Q(n) = true$.

  During the loop for $j$:

    Let $t = A[j+1]$ at the beginning of the loop.

    Then $t$ is before all elements in $A[j+2..n]$ because $Q(j+1) = true$.

    At the end of the loop:

      $t = A[j]$ or $t = A[j+1]$.

      Also $A[j] \le A[j+1]$.

      Thus $A[j] \le t$ and hence $A[j]$ is before all elements in $A[j+1]$.

    Therefore $Q(j) = true$.

  Therefore by induction $Q(i) = true$ and hence $A[i]$ is before all elements in $A[i+1..n]$.

  Also $A[1..i-1]$ is still sorted and before $A[i]$ because only $A[i..n]$ were permuted.

  Thus $A[1..i]$ is sorted and before all elements in $A[i+1..n]$.

  Therefore $P(i) = true$.

Therefore by induction $P(n) = true$ and hence $A[1..n]$ is sorted.