制御フロー：まとめと挑戦課題

単元で達成したこと

この単元は、分岐とループで実行の順序を制御し、その正しさについて推論することを教えようとした。すべての場合が処理されること、すべてのループがなすべきことをなし、停止すること、である。この目的は、導入が既知と宣言したことだけに基づいて果たされた。第 3 単元の条件、第 2 単元の型、そしてレッスン 1.1 のトレースと変量である。最大公約数を三つの固定した手順で計算し、データによっては誤った答えを出したり 0 で割ったりしたプログラムは、三行のループに置き換えられ、今ではそのループがすべての負でないデータについて正しいことを証明できる。

分岐

レッスン 分岐 は、常に波括弧をつけた if 文を教えた。else if の連鎖では条件が真である最初の枝が実行されること、したがって各枝の実際の場合はその条件とそれより前のすべての条件の否定とを合わせたものであることを示した。順序が重要であること、そして枝が警告なしに到達不能になりうることは、ここから来る。あらゆる分岐の正しさの基準を定めた。その場合は互いに重ならず（連鎖の形がそれを保証する）、網羅的でなければならず（else で終われば網羅的である）、さらに仕様の場合と一致しなければならない。これは各場合の内部と各境界の両側で確かめる。二つの短い値のどちらかを、分岐をまるごと書かずに選ぶための条件演算子を紹介した。最後に enum class と switch を扱った。後者で場合を書き忘れると、コンパイラが警告する。

ループ

レッスン ループ は、while、do、for を一つの仕組みの三つの形として示した。while は各周回の前に条件を計算し、一度も周回しないことがある。do は少なくとも一度周回する。for は初期化、条件、更新をヘッダにまとめ、そのループ変数はループのなかでだけ生きる。それらの同値性と、トレース表を教えた。条件によって停止する while では条件の計算が $k + 1$ 回、周回が $k$ 回である（do では計算が $k$ 回）。またヘッダから周回数を数えることを教え、これが 1 ずれのエラーを防ぐ。break、continue、入れ子のループを加えた。入れ子のループの内側の本体が実行される回数は和で与えられ、範囲が固定なら $m \cdot p$、三角形なら $n(n + 1)/2$ である。

正しいループの設計

レッスン 正しいループの設計 は、ループを設計の対象にした。パターン（カウンタ、累積変数、最大値と最小値、番兵、フラグ）を集め、それぞれを各周回の後にその変数が何を意味するかによって定義した。不変条件を、条件が計算されるたびに成り立つ主張として定義し、その三つの義務、すなわち初期条件、維持、終了を示した。終了は偽の条件とあわせて事後条件を与える。そして不変条件を周回数についての帰納法として捉えた。事後条件から不変条件へ、不変条件から本体へと逆向きに設計することを教えた。停止性を変量で正当化し、C++ の算術が変量を無効にする三つのループを示した。1.0 を飛び越える実数のループ、一周してしまう符号なしのカウンタ、オーバーフローする符号付きのカウンタである。最後に、デバッガとの最初の出会いを用意した。

数値アルゴリズム

レッスン 数値アルゴリズム は、以上を四つの古典的なアルゴリズムに適用した。どれも main のなかに書かれ、証明された。試し割りによる素数判定では、$\sqrt{n}$ まで調べれば十分であるという命題と、条件 d <= n / d を扱った。この条件は、d * d <= n がオーバーフローするところでもオーバーフローしない。ユークリッドの互除法では、不変条件 $\operatorname{gcd}(a, b) = \operatorname{gcd}(a_0, b_0)$ と変量 $b$、そして C++ における二つの危険、すなわち負の結果と、条件を本体の後で計算した場合の 0 による除算を扱った。逐次除算による基数変換と、係数一つにつき乗算一回で多項式の値を計算するホーナー法を扱った。そして二分法を扱った。これは中間値の定理によって保証され、整数のカウンタによって制御され、その周回数は前もって計算できる。