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.

Solution 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.

Solution 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)

Solution 3

Generally speaking, you would attempt a proof by induction to show correctness. This works very well when proving correctness of recursive functions, since you can prove the base case directly, and then can use the fact that the function works for "smaller" inputs in order to prove that it works for the next largest input.

In this case, I'd attempt a proof by well-founded induction. Specifically, I'd prove that

1. The function is correct for all inputs of the form (n, 0).
2. Assuming that for all inputs (n', k') such that (n', k') is lexicographically less than (n, k), the function is correct, prove that it is correct for (n, k).

The specifics of this proof would need to leverage the specifics of your function and the bahvaior of binomial coefficients, but the general template is as above.

Hope this helps!