Merge
General Information
Algorithmic problem: Merging two sorted sequences
Type of algorithm: loop
Auxiliary data: There are two current positions: [math]\displaystyle{ i_1 \in \{0,\dots,|S_1|\} }[/math] and [math]\displaystyle{ i_2 \in \{0,\dots,|S_2|\} }[/math] .
Abstract View
Invariant: Before and after each iteration prior to termination:
- [math]\displaystyle{ S }[/math] consists exactly of all elements [math]\displaystyle{ S_1[1],\dots,S_1[i_1] }[/math] and [math]\displaystyle{ S_2[1],\dots,S_2[i_2] }[/math].
- [math]\displaystyle{ S }[/math] is sorted according to the comparison on [math]\displaystyle{ S_1 }[/math] and [math]\displaystyle{ S_2 }[/math].
Variant: [math]\displaystyle{ i_1 + i_2 }[/math] increases by [math]\displaystyle{ 1 }[/math] (prior to termination); neither [math]\displaystyle{ i_1 }[/math] nor [math]\displaystyle{ i_2 }[/math] decreases.
Break condition: [math]\displaystyle{ i_1 = |S_1| }[/math] or [math]\displaystyle{ i_2 = |S_2| }[/math].
Induction Basis
Abstract view: [math]\displaystyle{ i_1 := 0 }[/math] and [math]\displaystyle{ i_2 := 0 }[/math].
Implementation: Obvious.
Proof: Nothing to show.
Induction Step
Abstract view:
- If [math]\displaystyle{ i_1 = |S_1| }[/math], append [math]\displaystyle{ S_2[i_2 + 1],\ldots,S_2[|S_2|] }[/math] at the end of [math]\displaystyle{ S }[/math] (in this order) and terminate the algorithm.
- Otherwise, if [math]\displaystyle{ i_2 = |S_2| }[/math], append [math]\displaystyle{ S_1[i_1 + 1],\ldots,S_1[|S_1|] }[/math] at the end of [math]\displaystyle{ S }[/math] (in this order) and terminate the algorithm.
- Otherwise, if [math]\displaystyle{ S_1[i_1 +1] \lt S_2[i_2 +1] }[/math], append [math]\displaystyle{ S_1[i_1 +1] }[/math] at the of [math]\displaystyle{ S }[/math] and increase [math]\displaystyle{ i_1 }[/math] by [math]\displaystyle{ 1 }[/math].
- Otherwise, append [math]\displaystyle{ S_2[i_2 +1] }[/math] at the of [math]\displaystyle{ S }[/math] and increase [math]\displaystyle{ i_2 }[/math] by [math]\displaystyle{ 1 }[/math].
Implementation: Obvious.
Correctness: Obvious.
Complexity
Statement: The complexity is in [math]\displaystyle{ \Theta(T\cdot(|S_1| + |S_2|)) }[/math] in the best and worst case, where [math]\displaystyle{ T }[/math] is the complexity of the comparison.
Proof: Obvious.