情報科学 › ソフトウェア設計とテスト › ビルドと依存関係
菱形の依存と高いほうの副版
プログラムが A と B に依存し、A はライブラリ C の版 の契約だけを使って、B は同じ主版の の契約だけを使って、それぞれ自分の正しさ（C の操作を呼び出すコードについての Hoare の三つ組）を証明しているとする。C が意味的バージョニングの約束（定義 8.6）を守っているならば、C の版を の 1 つにしても、A と B の証明した三つ組はどちらも成り立つ。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 6 件、定義なども含めて 8 件）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義（直接 1 件）
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
置換原則✓定理 7.2・契約による設計
Hoare 論理の健全性✓定理 3.8・契約による設計
代入の規則は後ろ向きである✓命題 3.6・契約による設計
- 表明への代入定義 3.4・契約による設計
これを使っている定理
証明で明示的に参照している定理は、まだありません。