title: General proof strategies to show correctness of recursive functions?
body: <p>I'm wondering if there exists any rule/scheme of proceeding with proving algorithm correctness? For example we have a function $F$ defined on the natural numbers and defined below:</p>
  
  <pre><code>function F(n,k)
  begin
    if k=0 then return 1
    else if (n mod 2 = 0) and (k mod 2 = 1) then return 0
    else return F(n div 2, k div 2);
  end;
  </code></pre>
  
  <p>where $n \ \text{div}\ 2 = \left\lfloor\frac{n}{2}\right\rfloor$</p>
  
  <p>the task is to prove that $F(n,k)= \begin{cases} 1  \Leftrightarrow  {n \choose k} \ \text{mod} \ 2 = 1 \ 0 \text{ otherwise } \end{cases} $</p>
  
  <p>It does not look very complicated (am I wrong?), but I don't know how does this kind of proof should be structured. I would be very grateful for help.</p>