停止性の証明？

プログラムが必ず終了するか？　無限ループにならないか？　　の証明。
これであってるのかな？

例題：階乗。言語はVDMで。

階乗: nat +> nat
階乗(n) == if n=0 then 1 else n*階乗(n-1);

n=0のとき
停止するか？：階乗(0)
停止するか？：if 0=0 then 1 else 0*階乗(0-1);
停止するか？：1
停止するか？：YES

n=kのとき、階乗(k)は停止すると仮定する。
n=k+1のとき
停止するか？：階乗(k+1)
停止するか？：if (k+1)=0 then 1 else (k+1)*階乗((k+1)-1);
停止するか？：(k+1)*階乗((k+1)-1);
停止するか？：階乗((k+1)-1);
停止するか？：階乗(k);
ここで、階乗(k)は停止すると仮定しているので、
停止するか？：YES

一般的には引数は複数だし、いろんな型があるから証明は難しいよなぁ〜。
VDMにmeasureができたけど、どうつかうんだ？