Proof of correctness of algorithms (induction) I am reading Algorithm's Design Manual by S.Skiena and I have a hard time understanding and proving the correctness of algorithms. I should use proof by induction and when we talk about summations and proving their formulas I can do it, I have no problem understanding why it is correct. When I get a loop on the other hand, I cannot even get started. I have a hard time combining the Loop invariant (also finding it) and the proof.

For example the following is a complete mystery (i tried reading a few similar questions on SO, but I still don't get it)

function multiply(y, z)
    if z = 0 then return(0) else
    return(multiply(cy, ⌊z/c⌋) + y · (z mod c))


I understand that I am asking a lot, but is it possible for someone to try to explain it step by step ? I am learning the book on my own, this is not a homework and I am not trying to cheat on anything, I just do not understand it.
how do I include the if else statement in the proof?


In this example, the if statement describes the basic case and the else statement describes the inductive step.

Induction on $z$.

Basis: $z = 0$. 

$$ \text{multiply}(y,z) = 0 = y \times 0. $$

Induction Hypothesis: Suppose that this algorithm is true when $0 &lt; z &lt; k$. Note that we use strong induction (wiki).

Inductive Step: $z = k$. 

\begin{align}
\forall c&gt;0 : \text{multiply}(y,z) &amp;= \text{multiply}(cy, \lfloor \frac{z}{c} \rfloor) + y \cdot (z \text{ mod } c) \\
&amp;= cy\cdot\left\lfloor \frac{z}
{c}\right\rfloor+y\cdot (z \text{ mod } c) \\
&amp;= yz.
\end{align}