情報科学 › ソフトウェア設計とテスト › 事例研究
決定的な生成
文書の集合 から成果物（番号の表、索引、ページ）を作る手続きが決定的であるとは、成果物が だけの関数であること、すなわちファイルを読む順序・並列度・実行時刻・実行する計算機によらないことをいう。
閉包の状態
定義
定義は閉包の起点です（証明を要しません）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
これを使っている定理
証明で明示的に参照している定理は、まだありません。