情報科学 › ソフトウェア設計とテスト › 事例研究
構文的な検査は両立でき、意味的な検査は両立できない
(a) 条件 (U) を満たす文書の集合について、「解決できない参照」という性質 に対し、索引を作って各参照を引く検査は、必ず止まり、健全かつ完全である。
(b) チューリング完全なプログラミング言語 を固定し、各環境が のプログラムを 1 つ含むとする。性質 を「実行すると型エラーで停止するプログラムを含む環境」の集合とする。このとき、どんな入力に対しても必ず止まる検査で、 について健全かつ完全なものは存在しない。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 4 件、定義なども含めて 5 件）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義（直接 2 件）
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
識別子の一意性のもとでの解決の一意性✓定理 3.2・事例研究
- 健全な静的検査の不完全性✓定理 5.6・プログラミング言語論
これを使っている定理
証明で明示的に参照している定理は、まだありません。