Question

Assume that the inner loop works correctly. Using a loop-invariant proof for the outer loop, formally prove that your pseudo-code correctly sorts the given array. Be sure that your loop invariant and proof cover the initialization, maintenance, and termination conditions

Given code:

/**
 * a[0:n-1] is an array of n elements.
 * temp is a variable to facilitate exchange.
 */
BubbleSort(a, n)
Begin
  for k = 1 to n-1 increment by 1 do  // where, k is for the pass
    for j = 0 to n – k – 1 increment by 1 do  // this is for comparison
      if a[j] > a[j+1] then  
        Set temp = a[j];
        Set a[j] = a[j+1];
        Set a[j+1] = temp;
      endif
    endfor
  endfor
End

Answer 1

Loop invariant for outer loop:
before ith iteration the elements in list from index n-k to n-1 are sorted
Initialization:before the first iteration k=1, which is last element since only one element it is sorted
hence true, thus invariant satisfied
Maintenance: since inner loop works correctly, this can be easily verified by checking the invariant after each iteration of outer loop, in this case it is satisfied
Termination:(step to prove correctness)
when the loop terminates, k = n-1 , since from maintenance we know that list will be sorted from n-k to n-1
so, agian loop invariant is satisfied, this means list is sorted