General proof strategies to show correctness of recursive functions?

Question

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:

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;

where $n \ \text{div}\ 2 = \left\lfloor\frac{n}{2}\right\rfloor$

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} $

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.

Answer 1

Correctness of recursive algorithms is often proven by mathematical induction. This method consists of two parts: first, you establish the basis, and then you use an inductive step.

In your case, the basis is all cases when k=0, or when k is odd but n is even.

The inductive step requires proving that when f(n,k) is correct, f(2*n,2*k), f(2*n+1,2*k), f(2*n,2*k+1) and f(2*n+1,2*k+1) are all correct.

Answer 2

Outside of proving your logic mathematically (example: inductive proof), there are some results in computing science related to this.

You can start here for an outline of the subject: Correctness
For your particular case, you'd be interested in partial correctness to show that the answer is the intended one. Then total correctness to show that the program terminates.

Hoare logic can solve your partial correctness.

As for the termination for this particular problem:

If (n%2==0 and k%1==1) or (k==0) the program terminates, otherwise it recurses to the n/2, k/2 case.
Using strong induction on k, we can show that the program always reaches one of the terminal nodes where k==0. (It may terminate earlier on the first clause but we only needed to show that it terminates at all, which this does)

So I've left the proof of partial correctness to you (because I don't know that stuff)