There is a huge variety of feasible approaches. Which is best suited depends on
- what you are trying to show,
- how much detail you want or need.
If the algorithm is a widely known one which you use as a subroutine, you often remain at a higher level. If the algorithm is the main object under investigation, you probably want to be more detailed. The same can be said for analyses: if you need a rough upper runtime bound you proceed differently from when you want precise counts of statements.
I will give you three examples for the well-known algorithm Mergesort which hopefully illustrate this.
High Level
The algorithm Mergesort takes a list, splits it in two (about) equally long parts, recurses on those partial lists and merges the (sorted) results so that
the end-result is sorted. On singleton or empty lists, it returns the input.
This algorithm is obviously a correct sorting algorithm. Splitting the list and merging it can each be implemented in time $\Theta(n)$, which gives us a recurrence for worst case runtime $T(n) = 2T\left(\frac{n}{2}\right) + \Theta(n)$. By the Master theorem, this evaluates to $T(n) \in \Theta(n\log n)$.
Medium Level
The algorithm Mergesort is given by the following pseudo-code:
procedure mergesort(l : List) {
if ( l.length < 2 ) {
return l
}
left = mergesort(l.take(l.length / 2)
right = mergesort(l.drop(l.length / 2)
result = []
while ( left.length > 0 || right.length > 0 ) {
if ( right.length == 0 || (left.length > 0 && left.head <= right.head) ) {
result = left.head :: result
left = left.tail
}
else {
result = right.head :: result
right = right.tail
}
}
return result.reverse
}
We prove correctness by induction. For lists of length zero or one, the algorithm is trivially correct. As induction hypothesis, assume mergesort performs correctly on lists of length at most $n$ for some arbitrary, but fixed natural $n>1$. Now let $L$ be a list of length $n+1$. By induction hypothesis, left and right hold (non-decreasingly) sorted versions of the first resp. second half of $L$ after the recursive calls. Therefore, the while loop selects in every iteration the smallest element not yet investigated and appends it to result; thus result is a non-increasingly sorted list containing all elements from left and right. The reverse is a non-decreasingly sorted version of $L$, which is the returned -- and desired -- result.
As for runtime, let us count element comparisons and list operations (which dominate the runtime asymptotically). Lists of length less than two cause neither. For lists of length $n>1$, we have those operations caused by preparing the inputs for the recursive calls, those from the recursive calls themselves plus the while loop and one reverse. Both recursive parameters can be computed with at most $n$ list operations each. The while loop is executed exactly $n$ times and every iteration causes at most one element comparison and exactly two list operations. The final reverse can be implemented to use $2n$ list operations -- every element is removed from the input and put into the output list. Therefore, the operation count fulfills the following recurrence:
$\qquad \begin{align}T(0) = T(1) &= 0 \\
T(n) &\leq T\left(\left\lceil\frac{n}{2}\right\rceil\right) + T\left(\left\lfloor\frac{n}{2}\right\rfloor\right) + 7n\end{align}$
As $T$ is clearly non-decreasing, it is sufficient to consider $n=2^k$ for asymptotic growth. In this case, the recurrence simplifies to
$\qquad \begin{align}T(0) = T(1) &= 0 \\
T(n) &\leq 2T\left(\frac{n}{2}\right) + 7n\end{align}$
By the Master theorem, we get $T \in \Theta(n \log n)$ which extends to the runtime of mergesort.
Ultra-low level
Consider this (generalised) implementation of Mergesort in Isabelle/HOL:
types dataset = "nat * string"
fun leq :: "dataset \<Rightarrow> dataset \<Rightarrow> bool" where
"leq (kx::nat, dx) (ky, dy) = (kx \<le> ky)"
fun merge :: "dataset list \<Rightarrow> dataset list \<Rightarrow> dataset list" where
"merge [] b = b" |
"merge a [] = a" |
"merge (a # as) (b # bs) = (if leq a b then a # merge as (b # bs) else b # merge (a # as) bs)"
function (sequential) msort :: "dataset list \<Rightarrow> dataset list" where
"msort [] = []" |
"msort [x] = [x]" |
"msort l = (let mid = length l div 2 in merge (msort (take mid l)) (msort (drop mid l)))"
by pat_completeness auto
termination
apply (relation "measure length")
by simp+
This already includes proofs of well-definedness and termination. Find an (almost) complete correctness proof here.
For the "runtime", that is number of comparisons, a recurrence similar to the one in the prior section can be set up. Instead of using the Master theorem and forgetting the constants, you can also analyse it to get an approximation that is asymptotically equal the true quantity. You can find the full analysis in [1]; here is a rough outline (it does not necessarily fit the Isabelle/HOL code):
As above, the recurrence for the number of comparisons is
$\qquad \begin{align}f_0 = f_1 &= 0 \\
f_n &= f_{\left\lceil\frac{n}{2}\right\rceil} + f_{\left\lfloor\frac{n}{2}\right\rfloor} + e_n\end{align}$
where $e_n$ is the number of comparisons needed for merging the partial results². In order to get rid of the floors and ceils, we perform a case distinction over whether $n$ is even:
$\qquad \displaystyle \begin{cases}
f_{2m} &= 2f_m + e_{2m} \\
f_{2m+1} &= f_m + f_{m+1} + e_{2m+1}
\end{cases}$
Using nested forward/backward differences of $f_n$ and $e_n$ we get that
$\qquad \displaystyle \sum\limits_{k=1}^{n-1} (n-k) \cdot \Delta\kern-.2em\nabla f_k = f_n - nf_1$.
The sum matches the right-hand side of Perron's formula. We define the Dirichlet generating series of $\Delta\kern-.2em\nabla f_k$ as
$\qquad \displaystyle W(s) = \sum\limits_{k\geq 1} \Delta\kern-.2em\nabla f_k k^{-s} = \frac{1}{1-2^{-s}} \cdot \underbrace{\sum\limits_{k \geq 1} \frac{\Delta\kern-.2em\nabla e_k}{k^s}}_{=:\ \boxminus(s)}$
which together with Perron's formula leads us to
$\qquad \displaystyle f_n = nf_1 + \frac{n}{2\pi i} \int\limits_{3-i\infty}^{3+i\infty} \frac{\boxminus(s)n^s}{(1-2^{-s})s(s+1)}ds$.
Evaluation of $\boxminus(s)$ depends on which case is analysed. Other than that, we can -- after some trickery -- apply the residue theorem to get
$\qquad \displaystyle f_n \sim n \cdot \log_2(n) + n \cdot A(\log_2(n)) + 1$
where $A$ is a periodic function with values in $[-1,-0.9]$.
- Mellin transforms and asymptotics: the mergesort recurrence by Flajolet and Golin (1992)
- Best case: $e_n = \left\lfloor\frac{n}{2}\right\rfloor$
Worst case: $e_n = n-1$
Average case: $e_n = n - \frac{\left\lfloor\frac{n}{2}\right\rfloor}{\left\lceil\frac{n}{2}\right\rceil + 1} - \frac{\left\lceil\frac{n}{2}\right\rceil}{\left\lfloor\frac{n}{2}\right\rfloor + 1}$
