情報科学 › ソフトウェア設計とテスト › テストの理論

経路の爆発と実行可能性

命題 3.7（「テストの理論」§3）・ ✓公理まで証明済み

条件分岐（判定 1 つと、真の側・偽の側それぞれ 1 つの文、合流点）を $n$ 個直列につないだ制御フローグラフには、入口から出口への歩道がちょうど $2^n$ 本ある。 $i$ 番目の判定が入力の第 $i$ ビットを調べるなら、そのすべてが実行可能である。
ループを含むプログラムでは、実行可能な経路が無限にありうる。
$\mathcal{L}$ をチューリング完全なプログラミング言語とする。 $\mathcal{L}$ のプログラムとその中の文が与えられたとき、その文が実行可能（ある入力で実行される）かどうかは決定可能でない。プログラムから実行可能な文の個数（文網羅の「100%」の分母）を計算するアルゴリズムも存在しない。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 10 件、定義なども含めて 13 件）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

前提をたどる証明が使う定理・定義（直接 3 件）

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

数学的帰納法の原理✓定理 3.2・証明の技術
- 背理法の正当性✓命題 6.2・証明の技術
- 整列性公理 3.1・証明の技術
停止問題定義 7.1・計算可能性
停止問題の決定不能性✓定理 7.2・計算可能性
- チューリング計算可能なら部分再帰的✓定理 5.4・計算可能性
  - クリーネの標準形定理✓定理 5.3・計算可能性
    1 ステップの算術化✓補題 5.2・計算可能性この先をたどる →
- 部分再帰関数はチューリング計算可能✓定理 6.2・計算可能性

これを使っている定理証明で参照している 1 件

文の削除の突然変異体と文網羅、等価性の判定✓命題 6.2・テストの理論