Bubble sort
General Information
Algorithmic problem: Sorting based on pairwise comparison
Type of algorithm: loop
Abstract View
Invariant: After [math]\displaystyle{ i \geq 0 }[/math] iterations, the elements of [math]\displaystyle{ S }[/math] at the positions [math]\displaystyle{ |S|-i+1,\dots,|S| }[/math] are placed at their ocrrect positions in sorting order.
Variant: [math]\displaystyle{ i }[/math] increases by [math]\displaystyle{ 1 }[/math].
Break condition: [math]\displaystyle{ i = |S| -1 }[/math]
Induction Basis
Abstract view: Nothing to do.
Implementation: Nothing to do.
Proof: Nothing to show.
Induction Step
Abstract view: Step-by-step, move the maximum element seen so far to the position [math]\displaystyle{ |S| - i + 1 }[/math].
Implementation: For [math]\displaystyle{ j := 2,\dots,|S|-i+1 }[/math] (in this order). If [math]\displaystyle{ S[j-1] \gt S[j] }[/math], swap [math]\displaystyle{ S[j-1] }[/math] and [math]\displaystyle{ S[j] }[/math].
Correctness: The loop invariant of the inner loop is this: after [math]\displaystyle{ m }[/math] iterations of the inner loop, [math]\displaystyle{ S[m+1] }[/math] is the maximum out of [math]\displaystyle{ S[1],\dots,S[m+1] }[/math]. To see that invariant, note that the induction hypothesis implies for an iteration on index [math]\displaystyle{ j }[/math] that [math]\displaystyle{ S[j-1] }[/math] is the maxiumum out of [math]\displaystyle{ S[1],\dots,S[j-1] }[/math]. So if [math]\displaystyle{ S[j-1] \gt S[j] }[/math]. [math]\displaystyle{ S[j-1] }[/math] is also the maximum out of [math]\displaystyle{ S[1],\dots,S[j] }[/math]. Therefore, swapping [math]\displaystyle{ S[j-1] }[/math] and [math]\displaystyle{ S[j] }[/math] maintains the invariant. On the other hand, if [math]\displaystyle{ S[j-1] \leq S[j] }[/math]. [math]\displaystyle{ S[j] }[/math] is already the maximum, so doing nothing maintains the invariant in this case.
Pseudocode
BUBBLESORT(A)
1 for i = 1 to "A.length" - 1
2 for j = A.length downto i + 1
3 if A[j] < A[j - 1]
4 exchange A[j] with A[j - 1]
Complexity
Statemen: The asymptotic complexity is in [math]\displaystyle{ \Theta(T\cdot n^2) }[/math] in the best and worst case, where [math]\displaystyle{ T }[/math] is the complexity of the comparison.
Proof: The asymptotic complexity of the inner loop in the [math]\displaystyle{ i }[/math]-th iteration of the outer loop is in [math]\displaystyle{ \Theta(T\cdot(n - i)) }[/math]. Therefore, the total complexity is in [math]\displaystyle{ \Theta \left( T\cdot\sum_{i=1}^{n-1} (n-i) \right) = \Theta \left( T\cdot\sum_{i=1}^{n-1} i \right) = \Theta \left( T\cdot\frac{n(n-1)}{2}\right) = \Theta(T\cdot n^2) }[/math]