"すべての例を挙げることはできない。だが、正しさの性質を記述することはできる。"

多くのテストは具体例に依存する。
与えられた入力と出力のペアが正しいかどうかを検証する――それは基本的な戦略であり、同時に限界を持つ。

Rustにおけるプロパティベーステスト（PBT）は、この限界に対する応答である。
それは「例を挙げるのではなく、性質を語ることで設計を検証する」という、より抽象度の高い検証手法だ。

この章では、quickcheck クレートを中心に、PBTの美学とその設計的意義を読み解く。

テストの“例外性”からの脱却

従来の単体テストは、具体例に基づく。

#[test]
fn adds_two() {
    assert_eq!(add(2, 2), 4);
}

だがこのテストが保証しているのは、「2 + 2 は 4」である、という点の正しさでしかない。

この点に対して、プロパティベーステストはこう考える：

「任意の a と b に対して、add(a, b) は b + a に等しいべきでは？」
「境界値や予期せぬデータで壊れない保証はあるか？」

つまり、特定の入力ではなく、入力空間全体に対する性質そのものを構文で記述するのがPBTの思想である。

quickcheck：性質の表現言語

Rustには、Haskell由来の quickcheck クレートが存在する。

use quickcheck::quickcheck;

fn reverse_reverse_is_identity(xs: Vec<u32>) -> bool {
    let reversed = xs.clone().into_iter().rev().collect::<Vec<_>>();
    reversed.into_iter().rev().collect::<Vec<_>>() == xs
}

quickcheck! {
    fn test_reverse_reverse(xs: Vec<u32>) -> bool {
        reverse_reverse_is_identity(xs)
    }
}

この構文は、以下を意味する：

Vec<u32> 型のあらゆる入力をランダムに生成し
関数が満たすべき「性質」をブール値で記述し
その性質が崩れる最小の入力を探索する

これは**「性質の記述＝設計の検証」**という文法的契約である。

設計とは“性質の集合”である

設計とは、本質的に「この関数はこう振る舞うべきだ」という性質の集積である。
例ではなく、性質こそが関数の定義に近い。

たとえば：

len(a + b) == len(a) + len(b)：結合における長さの保存
sort(sort(x)) == sort(x)：安定性の検証
parse(serialize(x)) == x：シリアライズの同一性保証

これらはすべて、構文で書ける保証の形である。
そして quickcheck は、その性質をコードとして自動実行可能な保証装置に変える。

“無限のテスト”を“構文で抑える”という逆説

PBTでは、すべてのケースを網羅することはできない。
だが、テストケースを自動生成することで、“想定外”を想定内に引き込む構造を構築できる。

これは、次のような特性を持つ：

多様な入力パターンに対して高い信頼性
複雑な境界ケースでの自動検出
構造的バグの最小入力としての“縮小（shrink）”

つまり、**“入力の無限性を構文の有限性で取り囲む”**という構造化手法である。

性質を書くという行為は、設計に責任を持つということ

関数の仕様が曖昧なとき、PBTは成立しない。
逆に言えば、PBTを書くためには、関数がどう振る舞うべきかを設計者が自覚していなければならない。

これは設計倫理の問題だ：

“この関数はどのような性質を守るべきか？”
“それは常に成り立つものか？”
“例外はあるのか？ならばなぜ？”

性質を書くことは、設計者がコードの意味と限界を構文で引き受ける行為に他ならない。

プロパティベーステストの文化的意義

Rustは、ただ安全な言語ではない。
それは設計を言語化し、構文として共有可能にする文化を持っている。

#[test]：命題の断片
quickcheck!：命題の普遍化
assert! → forall: 特定から汎化へ

この進化は、コードが「ロジック」ではなく「理論」として語られる世界への遷移を意味している。

結語：性質こそが、設計の語彙である

プロパティベーステストとは、設計を論理式に分解し、それを構文として検証する構造的試みである。
quickcheck のようなツールは、その文脈をRustに持ち込み、例を超えた信頼性の設計を可能にする。

具体例で語れるのはコードの断片だけだ。
性質で語ることで、設計の本質を構文化することができる。

"すべてをテストすることはできない。だが、設計の正しさを語る言葉なら、構文にできる。"