変数 X がある数 x を持つ状態で fact_com を実行すると、 変数 Y が x の階乗の値を持つ状態で停止する、ということを示したくなります。これを示すため、ループ不変式 (loop invariant) という重要な概念を使います。 Z := X; Y := 1; WHILE not (Z = 0) D…

とりあえず、Software Foundationsを読みすすめるのは中断して、 始めからもう一度ゆっくり読んで行くことにする。新しいほうがなんとなく初心者に優しいような気もするのでそっちを。 エイゴムズカシイデス