Recursive Algorithms and Programme Correctness