whileの意味

計算モデル論では、LCモデルによって命令の意味の表現と、プログラムが正しく終了することの表現について。「命令の列」と「メモリ状態」をひとセットとして、これを公式に従って変形していき、最終的な形に落ち着くならプログラムは正常終了する。そして命令列を変形する公式のセットが、命令の意味を表現しています。ifとwhileだけを使ったプログラム構造はこの枠組みで意味表現が可能です。gotoが入り込むと途端に難しくなるらしいので、それはまた来週。