2-2  Correctness of bubblesort

Bubblesort is a popular algorithm.  It works by repeatedly swapping adjacent elements that are out of order.

Bubblesort(A)
1 for i <- 1 to length[A]
2    do for j <- length[A] downto i + 1
3        do if A[j] < A[j-1]
4              then exchange A[j] <-> A[j-1]

a. Let A' denote the output of Bubblesort(A).  To prove that Bubblesort is correct, we need to prove that it terminates and that

A'[1] <= A'[2] <= ... <= A'[n]     ... (2.3)

where n = length[A].  What else must be proved to show that Bubblesort actually sorts?

The next two parts will prove inequality (2.3)

b. State precisely a loop invariant for the for loop in lines 2-4, and prove that this loop invariant holds.  Your proof should use the structure of the loop invariant proof presents in Chapter 2 (CLR).

c. Using the termination condition of the loop invariant proved in part (b), state a loop invariant for the for loop in lines 1-4 that will allow you to prove inequality (2.3).  Your proof should use the structure of the loop invariant proof presented in Chapter 2 (CLR).

d. What is the worse-case running time of Bubblesort? How does it compare to the running time of insertion sort?