情報科学 › ソフトウェア設計とテスト › ビルドと依存関係

ロックファイルによる取得の決定性

命題 8.4（「ビルドと依存関係」§8） ・ ✓公理まで証明済み

解決 ρ\rho と、選ばれた各版の配布物の内容ハッシュを記録した表

ℓ={(a, ρ(a), ha):a は ρ の定義域に属する}\ell = \{(a,\ \rho(a),\ h_a) : a \text{ は } \rho \text{ の定義域に属する}\}

をロックファイルという。取得の手続きを「各 (a,v,h)∈ℓ(a, v, h) \in \ell について、配布元から aa の版 vv の内容 cc を取り、H(c)=hH(c) = h ならば採用し、そうでなければ失敗して止まる」と定める。HH が現れる内容の上で単射ならば、取得が成功したときに得られる内容の族 (ca)a(c_a)_a は ℓ\ell だけで決まり、取得の時刻・配布元の状態・取得する計算機によらない。

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

閉包の状態

✓ 公理まで証明済み

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

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

前提をたどる 証明が使う定理・定義

証明は Rikai の他の定理を参照していません（定義と論理だけで示されています）。

これを使っている定理

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

関連するノック 1 問