プログラムが必ず終了するか？ 無限ループにならないか？ の証明。 これであってるのかな？ 例題：階乗。言語はVDMで。 階乗: nat +> nat 階乗(n) == if n=0 then 1 else n*階乗(n-1); n=0のとき 停止するか？：階乗(0) 停止するか？：if 0=0 then 1 else 0*…