情報科学 › ソフトウェア設計とテスト › 継続的インテグレーション
依存グラフによるテストの選択の安全性
テストを 前章 のビルドの記述のタスクとして表し、テスト の出力（合格・不合格）を と書く。記述は密閉的で（依存の宣言が完全で、テストの結果が宣言した依存だけで決まる）、前の版 ではすべてのテストが合格していたとする。版 で変更されたファイルの集合を 、 から依存グラフで到達できるタスクの集合を とする。このとき
が成り立つ。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 13 件、定義なども含めて 15 件）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義（直接 1 件）
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
増分ビルドの正しさ✓定理 4.2・ビルドと依存関係
クリーンビルドの一意性✓定理 4.1・ビルドと依存関係
トポロジカル順の存在と計算✓定理 3.2・ビルドと依存関係
- 2 つの表現の計算量✓命題 2.6・グラフアルゴリズム この先をたどる →
- 閉路のないグラフには入次数 0 の頂点がある✓補題 3.1・ビルドと依存関係 この先をたどる →
- 灰色頂点の構造✓補題 4.1・グラフアルゴリズム
- 有向閉路の検出✓定理 4.2・グラフアルゴリズム この先をたどる →
- 密閉性定義 2.2・ビルドと依存関係
- 完全帰納法✓定理 4.3・証明の技術（上で展開済み）
これを使っている定理
証明で明示的に参照している定理は、まだありません。