Proving tail-recursive function (calculating powers of an integer)

Question

Here's a function whose corectness I want to prove (written in OCaml):

let rec pow ak a k = if k=0 then ak
else if (k mod 2)=1 then pow (ak*a) (a*a) (k/2)
else pow ak (a*a) (k/2);;

Its specification:

For integers ak, a>0, k>=0 pow returns ak*(a^k).

I know I need to prove 2 things - that the function terminates, and returns the correct result for the assumed input. The problem is I haven't seen many proofs like that and the only thing I know is that I need to use induction. How should I approach such a problem?

ivg ivg · Accepted Answer · 2014-10-11T16:39:09

Prove the base case. Then prove that for a+1 and k+1 the statement is true in assumption that it works for a and k.

Proving tail-recursive function (calculating powers of an integer)

1 Answers