證明尾遞歸函數（計算整數的權力）

Question

這裏有一個功能我要證明其corectness（寫在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);; 

其規格：

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

我知道我需要證明2件事 - 函數終止，並返回假設輸入的正確結果。問題是我沒有看到這樣的證據，我唯一知道的是我需要使用歸納。我應該如何處理這樣的問題？

Answer 1

證明基礎案例。然後證明對於a+1和k+1，該聲明是假設它適用於a和k。