Общие стратегии доказательства для демонстрации правильности рекурсивных функций?

Интересно, существует ли какое-либо правило / схема доказательства правильности алгоритма? Например, у нас есть функция $ F $, определенная на натуральных числах и определенная ниже:

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;

где $ n \ \ text {div} \ 2 = \ left \ lfloor \ frac {n} {2} \ right \ rfloor $

задача состоит в том, чтобы доказать, что $ F (n, k) = \ begin {cases} 1 \ Leftrightarrow {n \ choose k} \ \ text {mod} \ 2 = 1 \ 0 \ text {else} \ end {case} $

Это не выглядит очень сложным (я ошибаюсь?), но я не знаю, как следует структурировать такого рода доказательства. Буду очень признателен за помощь.