情報科学 › ソフトウェア設計とテスト › 性質ベーステスト
種による再現
性質ベーステストの 1 回の実行が、擬似乱数生成器（定義 5.1［再現できる数値実験］）の出力列を受け取る「乱数を消費する決定的なプログラム」である、すなわち、入力の生成、性質 の評価、縮約、結果（合格か、報告する反例は何か）の出力が、受け取った乱数の値と初期状態だけで決まるとする。このとき、実行の結果は種だけで決まる。とくに、失敗した実行は、同じ種で実行し直せば、同じ反例とともに再現される。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 1 件、定義なども含めて 2 件）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義（直接 2 件）
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
これを使っている定理
証明で明示的に参照している定理は、まだありません。