第 6 章状態機械

状態機械 (state machine) はステップごとに進行する処理を抽象化するモデルである。コンピュータープログラムはステップごとに進行する計算処理を定義すると理解できるので、情報科学で状態機械がよく使われるのは不思議なことではない。他にも、デジタル回路の設計や確率過程のモデル化でも状態機械は利用される。本章では Floydフロイドの不変条件の原理 (invariant principle) を紹介する。これは状態機械に関する性質の証明で使いやすいように言い換えた数学的帰納法である。

情報科学で最も重要な数学的帰納法の使い方の一つが、何らかの処理の全てのステップで成り立つ性質の証明である。いくつかの操作を一つずつ実行するとき、各ステップの前後で保存される性質を保存不変条件 (preserved invariant) と呼ぶ。例えば「この飛行機の高度はフラップが展開されていない限り \(1{,}000\) フィート以上である」や「原発の原子炉はメルトダウンを起こさない温度に保たれる」は現実世界で保存不変条件となることが要求される性質の例である。