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

文の削除の突然変異体と文網羅、等価性の判定

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

$p$ を制御フローグラフによるプログラム、 $n$ をその文とし、 $n$ の効果 $a_n$ を恒等写像に置き換えた突然変異体を $p_{-n}$ とする。テスト集合 $T$ が（ $p$ の出力と比べるオラクルのもとで） $p_{-n}$ を殺すならば、 $n$ はある $x \in T$ の $p$ での実行経路に現れる。したがって、文の削除による突然変異体のうち等価でないものをすべて殺すテスト集合は、削除すると振る舞いが変わる文をすべて実行する。
$\mathcal{L}$ をチューリング完全なプログラミング言語とする。 $\mathcal{L}$ のプログラムとその突然変異体が等価であるかどうかは決定可能でない。したがって、突然変異スコアの分母を計算するアルゴリズムは存在しない。

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

閉包の状態

✓ 公理まで証明済み

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

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

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

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

伝播 ⇒ 感染 ⇒ 到達✓補題 2.5・テストの理論
- 数学的帰納法の原理✓定理 3.2・証明の技術
  - 背理法の正当性✓命題 6.2・証明の技術
  - 整列性公理 3.1・証明の技術
経路の爆発と実行可能性✓命題 3.7・テストの理論
- 数学的帰納法の原理✓定理 3.2・証明の技術（上で展開済み）
- 停止問題定義 7.1・計算可能性
- 停止問題の決定不能性✓定理 7.2・計算可能性（上で展開済み）
停止問題の決定不能性✓定理 7.2・計算可能性
- チューリング計算可能なら部分再帰的✓定理 5.4・計算可能性
  - クリーネの標準形定理✓定理 5.3・計算可能性
    1 ステップの算術化✓補題 5.2・計算可能性この先をたどる →
- 部分再帰関数はチューリング計算可能✓定理 6.2・計算可能性

これを使っている定理

証明で明示的に参照している定理は、まだありません。