情報科学 › ソフトウェア設計とテスト › 事例研究

文書ごとに独立な検査は並列化・増分化できる

命題 6.5（「事例研究」§6） ・ ✓公理まで証明済み

(a) 検査 κ\kappa が、各文書 dd の内容だけから決まる違反の集合 κd\kappa_d の和集合 κ(K)=⋃d∈Docκd\kappa(K) = \bigcup_{d \in \mathrm{Doc}} \kappa_d であるとする。このとき、文書をどの順序で、いくつに分けて並列に処理しても κ(K)\kappa(K) は同じである。また、文書 dd だけが変更されたとき、κd\kappa_d だけを計算し直して和集合を取り直せば、全体を計算し直した結果に一致する。

(b) 参照の検査の、文書 dd に関する部分 Ud={(d,e,r)∈U(K)}U_d = \{(d, e, r) \in U(K)\} は、dd の内容と索引 Idx(K)\mathrm{Idx}(K) の定義域（鍵の集合）から決まる。「鍵の集合を作るタスク」が全文書を依存に、「UdU_d を作るタスク」が dd と鍵の集合を依存に宣言していれば、増分的な実行の結果は全体を計算し直した結果に一致する。さらに、内容の比較による早期打ち切りのもとでは、文書 d′d' の変更が鍵の集合を変えないかぎり、d≠d′d \ne d' の UdU_d は再計算されない。

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

閉包の状態

✓ 公理まで証明済み

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

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

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

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

これを使っている定理

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