Merge: Difference between revisions
Jump to navigation
Jump to search
| Line 8: | Line 8: | ||
== Abstract View == | == Abstract View == | ||
'''''Invariant:''''' Before and after each iteration: | |||
# <math>S</math> consists exactly of all elements <math> S_1[1],\dots,S_1[i_1]</math> and <math> S_2[1],\dots,S_2[i_2]</math>. | |||
# <math>S</math> is sorted according to the comparison on <math>S_1</math> and <math>S_2</math>. | |||
'''''Variant:''''' <math>i_1 + i_2</math> increases by <math>1</math>; neither <math>i_1</math> nor <math>i_2</math> decreases. | |||
'''''Break condition:''''' <math>i_1 = |S_1|</math> and <math>i_2 = |S_2|</math>. | |||
== Induction Basis == | == Induction Basis == | ||
Revision as of 18:58, 25 September 2014
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:
- [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]; neither [math]\displaystyle{ i_1 }[/math] nor [math]\displaystyle{ i_2 }[/math] decreases.
Break condition: [math]\displaystyle{ i_1 = |S_1| }[/math] and [math]\displaystyle{ i_2 = |S_2| }[/math].