a-san https://blog.hatena.ne.jp/a-san/ a-sanの日記 https://a-san.hatenadiary.org/ プログラムが必ず終了するか？ 無限ループにならないか？ の証明。 これであってるのかな？ 例題：階乗。言語は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)… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fa-san.hatenadiary.org%2Fentry%2F20090729%2Fp1" title=" 停止性の証明？ - a-sanの日記" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2009-07-29 00:00:00 rich https://a-san.hatenadiary.org/entry/20090729/p1 1.0 100%