Bubble

General Information

Algorithmic problem: Moving the maximum element

Type of algorithm: loop

Abstract View

Invariant: After [math]\displaystyle{ i \geq 0 }[/math] iterations, the element at position [math]\displaystyle{ l + i }[/math] is the maximum of the elements at the position [math]\displaystyle{ l,\dots,l+i }[/math].

Variant: [math]\displaystyle{ i }[/math] increases by [math]\displaystyle{ 1 }[/math]

Break condition: [math]\displaystyle{ i = r - l }[/math]

Induction Basis

Abstract view: Nothing to do.

Implementation: Nothing to do.

Proof: Nothing to show.

Induction Step

Abstract view: Exchagne the elements at positions [math]\displaystyle{ l + i -1 }[/math] and [math]\displaystyle{ l + i }[/math] if necessary.

Implementation: If [math]\displaystyle{ S[l+i-1] \gt S[l+i] }[/math], swap [math]\displaystyle{ S[l+i-1] }[/math] and [math]\displaystyle{ S[l+i] }[/math].

Correctness: The induction hypothesis implies that, immediately before the [math]\displaystyle{ i }[/math]-th iteration, [math]\displaystyle{ S[l+i-1] }[/math] is the maximum of the elements at the positions [math]\displaystyle{ l,\dots,l+i-1 }[/math]. If [math]\displaystyle{ S[l+i-1] \gt S[l+i] }[/math], [math]\displaystyle{ S[l+i-1] }[/math] is also the maximum out of [math]\displaystyle{ 1,\dots,l+i }[/math] and should thus be moved to the position [math]\displaystyle{ l+i }[/math]. Otherwise [math]\displaystyle{ S[l+i] }[/math] is at least as large as all elements at positions [math]\displaystyle{ l+1,\dots,l+i-1 }[/math] and should thus stay at position [math]\displaystyle{ l+i }[/math].

Complexity

Statement: The asymptotic complexity is [math]\displaystyle{ \Theta(r-l) }[/math] in the best and worst case. Proof: Obvious.