# 性質ベーステスト：性質の書き方・生成・縮約と検出確率

> 入力を人が選ぶ代わりに、仕様を性質として書き入力を無作為に生成するテストを扱う。検出確率と必要な試行回数、境界値を混ぜた生成の効果、再帰的な生成器の大きさ、縮約の停止性、差分デバッグ ddmin の 1-最小性と実行回数、変成関係とモデルベーステストを証明し、Hypothesis の実行例を示す。
> https://rikai.mugen-giken.com/computer-science/software-design-testing/property-based-testing

## 0. この記事の要点

プログラムのテストでは、「この入力ならこの出力」という例を人が一つずつ用意するのが普通です。しかし、用意した例以外の入力で誤るプログラムは、そのテストをすり抜けます。この記事は、例を並べる代わりに「どんな入力でも成り立つはずのこと」を書き、入力は機械に大量に作らせる方法を扱います。読み終えると、何個試せば誤りがどのくらいの確率で見つかるか、見つかった失敗例をどう小さくして原因を探すかが分かります。

- **性質ベーステスト**は、「この入力にはこの出力」という例の代わりに、「すべての入力について成り立つべき命題」（性質）を書き、入力は生成器に無作為に作らせます。
- 性質を破る入力の割合（失敗率）が $\theta$ のとき、$N$ 個の独立な入力で反例が見つかる確率は $1 - (1 - \theta)^N$ です。確率 $1 - \delta$ で見つけるには $N \ge \ln(1/\delta)/\theta$ で足り、$N \lt (1 - \delta)/\theta$ では足りません。反例が出なかったことから言えるのは「この生成分布での $\theta$ が小さい」ことだけです。
- 特定の 1 点や境界だけで破れる性質は、一様な生成ではまず見つかりません。境界値・特殊値を混ぜた生成にすると、失敗率を下から抑えられます。
- 再帰的なデータの生成器は、子を作る確率 $p$ が $1/2$ を境に振る舞いが変わります。$p \lt 1/2$ なら大きさの期待値は $1/(1 - 2p)$、$p = 1/2$ では期待値が無限、$p \gt 1/2$ では正の確率で止まりません。
- 見つかった反例は**縮約**して小さくします。候補が自然数値の尺度を真に減らすなら、貪欲な縮約は必ず止まり、局所的に最小な反例を返します。差分デバッグ ddmin（失敗する入力から不要な部分を削っていく算法）は、1-最小（どの 1 要素を取り除いても失敗しなくなる）な反例を高々 $6n^2$ 回の実行で求め、原因が 1 要素なら $2\lceil \log_2 n \rceil$ 回で済みます。
- 正しい出力が分からない関数には**変成関係**（入力をこう変えたら出力はこう変わる、という関係）が、状態をもつ系には**参照モデルとの比較**が使えます。どちらも、検出できない誤りの集合を特定できます。

<Aside type="tip" title="この記事で使う事前知識">

- **確率変数**: 試行の結果に応じて値が決まる量。→ [確率変数](/mathematics/probability/random-variables#def-random-variable)
- **期待値**: 確率変数の値を、確率で重みづけして平均したもの。→ [期待値](/mathematics/probability/random-variables#def-expectation)
- **オラクル**: テストで、出力が正しいかどうかを判定する基準。→ [オラクル](/computer-science/software-design-testing/testing-theory#def-test-oracle)
- **同値分割と境界値**: 入力を同じ振る舞いの組に分け、組の境目の値を選んで試す方法。→ [同値分割と境界値](/computer-science/software-design-testing/testing-theory#def-equivalence-partition)
- **表現不変条件**: データ型の内部表現が、いつも満たしているべき条件。→ [表現不変条件](/computer-science/software-design-testing/contracts-and-invariants#def-rep-invariant)
- **ループ変量**: 繰り返しのたびに減り、有限回で止まることを保証する量。→ [ループ変量](/computer-science/software-design-testing/contracts-and-invariants#def-variant)

</Aside>

## 1. 動機

[前章](/computer-science/software-design-testing/testing-theory) の結論は 2 つありました。有限のテスト集合は、テストしなかった 1 点で誤る実装を通してしまう（<Ref to="computer-science/software-design-testing/testing-theory#thm-testing-incompleteness" />）。そして、どの入力を選ぶかの方法はどれも、誤りについての仮定に支えられている。人が入力を選ぶかぎり、選ぶ人が思いつかなかった場合はテストされません。実装した本人がテストを書くなら、実装で考え落とした場合は、テストでも考え落としている可能性が高い。

性質ベーステストは、入力を選ぶ仕事を機械に任せます。人が書くのは、個々の入力と期待値ではなく、**すべての入力について成り立つべき命題**です。「整列した結果は昇順である」「符号化して復号すると元に戻る」。入力は生成器が無作為にたくさん作り、命題を破る入力（反例）が見つかれば報告します。この方法は、K. Claessen と J. Hughes が 2000 年に発表した Haskell のライブラリ QuickCheck で広まり、いまでは多くの言語に同種の道具があります。この記事のコード例は Python の Hypothesis を使います。

無作為に入力を作るという方法は、乱暴に見えます。この記事では、それがどの程度あてになるのかを定理で確かめます。問いは 4 つです。(1) 何個試せば、どのくらいの確率で誤りが見つかるのか。(2) 入力をどういう分布で作るべきか。(3) 見つかった反例は大きくて読みにくいが、どう小さくするか、その手続きは止まるのか。(4) 正しい出力が分からない関数には、どんな性質を書けばよいのか。

同じ問いは、数値計算の検算でも現れます。[検算と検証](/computer-science/research-computing/verification-of-computations) は、乱数で作った行列で恒等式を確かめる方法と、その限界を扱っています。この記事は、その離散的な対象（列・木・操作の列）についての版にあたります。

## 2. 性質を書く

<Definition id="def-property" title="性質と反例">
$X$ を入力の集合とする。**性質**とは、写像 $\varphi : X \to \{\text{真}, \text{偽}\}$ であって、各 $x$ について $\varphi(x)$ の値をプログラムで計算できるものをいう。性質 $\varphi$ が主張するのは全称命題「すべての $x \in X$ について $\varphi(x)$ は真」である。$\varphi(x)$ が偽である $x$ を**反例**という。

これに対して、入力 $x_1, \ldots, x_r$ と期待される出力 $y_1, \ldots, y_r$ を人が選び、実装 $f$ について $f(x_i) = y_i$ を確かめるテストを**例示によるテスト**という。
</Definition>

性質 $\varphi$ は、前章の[オラクル](/computer-science/software-design-testing/testing-theory#def-test-oracle)（<Ref to="computer-science/software-design-testing/testing-theory#def-test-oracle" />）を入力の関数として書いたものです。実装 $f$ とオラクル $O$ に対して $\varphi(x) = [(x, f(x)) \in O]$ とおけば、$\varphi$ の反例は $f$ が不合格になる入力です。違いは、期待値を 1 つずつ書く代わりに、**どんな入力にも使える判定**を書くところにあります。

よく使われる性質の型を挙げます。

| 型 | 形 | 例 |
|---|---|---|
| 往復 | $\mathrm{decode}(\mathrm{encode}(x)) = x$ | 直列化と復元、圧縮と展開、構文解析と整形 |
| 冪等 | $f(f(x)) = f(x)$ | 整列、正規化、重複の除去 |
| 可換・結合 | $x \oplus y = y \oplus x$、$(x \oplus y) \oplus z = x \oplus (y \oplus z)$ | 集合の和、併合の操作 |
| 不変量 | $I(f(x))$ が成り立つ | 出力は昇順、木は平衡、残高は非負 |
| 単調性 | $x \preceq y \Rightarrow f(x) \preceq f(y)$ | 要素を足しても最大値は減らない |
| 参照実装との一致 | $f(x) = f_{\mathrm{ref}}(x)$ | 速い実装と、遅いが自明な実装 |
| 変成関係 | $f(g(x)) = h(f(x))$ | 入力を並べ替えても整列の結果は同じ |
| 代数的な恒等式 | $(A^{\mathsf{T}})^{\mathsf{T}} = A$、$(AB)^{\mathsf{T}} = B^{\mathsf{T}} A^{\mathsf{T}}$ | 行列の転置・逆行列 |

不変量の型は、[契約による設計](/computer-science/software-design-testing/contracts-and-invariants) の事後条件や[表現不変条件](/computer-science/software-design-testing/contracts-and-invariants#def-rep-invariant)を、そのまま性質にしたものです。性質ベーステストは、契約を無作為な入力で検査する方法だとも言えます。

1 つの性質が仕様のすべてを表しているとは限りません。次の例で確かめます。

<Example id="ex-sort-properties" title="整列の 3 つの性質と、重複を落とす誤り">
整列（<Ref to="computer-science/algorithms/sorting#def-sorting-problem" />）の実装に、重複する要素を落とす誤りを入れます。性質を 3 つ書きます。

```python
# test_sort.py — Python 3.12.14 / pytest 9.1.1 / hypothesis 6.168.5
from collections import Counter
from hypothesis import given, settings, strategies as st

def my_sort(xs):
    """誤りを入れた整列: 重複する要素を落としてしまう。"""
    return sorted(set(xs))

lists = st.lists(st.integers())
fixed = settings(derandomize=True, database=None, max_examples=200)   # 種を固定し、過去の反例の保存を使わない

@fixed
@given(lists)
def test_output_is_sorted(xs):
    ys = my_sort(xs)
    assert all(ys[i] <= ys[i + 1] for i in range(len(ys) - 1))

@fixed
@given(lists)
def test_idempotent(xs):
    assert my_sort(my_sort(xs)) == my_sort(xs)

@fixed
@given(lists)
def test_is_permutation(xs):
    assert Counter(my_sort(xs)) == Counter(xs)
```

`pytest test_sort.py -q` の出力の抜粋です。

```text
..F                                                                      [100%]
E       assert Counter({0: 1}) == Counter({0: 2})
E       Failing test case: test_is_permutation(
E           xs=[0, 0],
E       )
1 failed, 2 passed in 0.74s
```

読み取れることを 3 つ挙げます。

1. 「出力は昇順」と「冪等」は、この誤った実装でも成り立ちます。重複を落として並べた列は昇順で、もう一度同じことをしても変わりません。**性質が通ることは、実装が正しいことを意味しません。** 「出力は昇順」だけなら、つねに空の列を返す実装も通ります。
2. 「出力は入力の並べ替え」は破れ、反例 `[0, 0]` が報告されました。これは、重複を落とす誤りを示す最小の入力です。Hypothesis は最初に見つけた反例をそのまま報告せず、小さくしてから報告します（縮約。第 5 節）。
3. 「昇順」と「並べ替え」の 2 つを合わせると、出力は入力から一意に決まります（同じ多重集合を昇順に並べる方法は 1 通りです）。この 2 つの性質の組は仕様そのもので、正確なオラクルです。性質の組が**仕様を決めているか**、それとも一部を述べているだけかは、性質を書くときにいつも確かめる価値があります。

`derandomize=True` は入力の生成をテスト関数から決まる種で行う設定、`database=None` は以前の実行で見つけた反例の保存を使わない設定です。この 2 つで、上の出力は実行のたびに同じになります（第 8 節）。ただし同じになるのは、同じ版の Python・pytest・Hypothesis で実行した場合です。生成と縮約の手順は Hypothesis の版によって変わるので、この記事の Hypothesis の出力（報告される反例、とくに <Ref to="ex-heap-model" /> の操作列）は、コードの先頭に書いた版でのものです。末尾の実行時間は実行のたびに変わります。
</Example>

<Example id="ex-json-roundtrip" title="直列化の往復">
往復の性質は、書くのが簡単で、見つかる誤りが多い型です。Python の標準ライブラリの `json` について、「JSON にして戻すと元に戻る」を書きます。

```python
# test_json.py — Python 3.12.14 / pytest 9.1.1 / hypothesis 6.168.5
import json
from hypothesis import given, settings, strategies as st

values = st.recursive(st.none() | st.booleans() | st.integers() | st.text(),
                      lambda inner: st.lists(inner) | st.dictionaries(st.integers(), inner), max_leaves=10)

@settings(derandomize=True, database=None, max_examples=300)
@given(values)
def test_roundtrip(x):
    assert json.loads(json.dumps(x)) == x
```

```text
E       Failing test case: test_roundtrip(
E           x={0: None},
E       )
```

これは `json` の不具合ではありません。JSON のオブジェクトのキーは文字列だけなので、整数のキー `0` は文字列 `"0"` になり、戻しても整数には戻りません。破れたのは実装ではなく、**私たちが書いた性質**（往復が成り立つ値の範囲についての思い込み）のほうです。性質ベーステストは、実装の誤りと同じくらい、仕様の理解の誤りを見つけます。キーを文字列に限れば（`st.dictionaries(st.text(), inner)`）、この性質は成り立つべきものになります。往復が成り立つ入力の範囲を正確に述べることが、そのまま直列化の契約の事前条件になります。
</Example>

## 3. 何個試せば見つかるか

### 3.1. 生成器と失敗率

<Definition id="def-generator" title="生成器・生成分布・失敗率">
**生成器**とは、乱数の列から入力の集合 $X$ の元を作る手続きをいう。生成器が作る入力は $X$ に値をとる確率変数で、その分布 $\mu$ を**生成分布**という。多くの生成器は**大きさのパラメータ** $s$（列の長さの上限、木の深さの上限、整数の絶対値の上限など）をもち、$s$ ごとに分布 $\mu_s$ が決まる。

性質 $\varphi$ の、生成分布 $\mu$ のもとでの**失敗率**を、反例の集合の確率
$$
\theta = \mu(\{\, x \in X \mid \varphi(x) \text{ は偽} \,\})
$$
と定める。
</Definition>

失敗率は性質だけでは決まらず、生成分布との組で決まります。同じ誤りでも、生成の仕方によって見つかりやすさが変わります。

<Theorem id="thm-detection-probability" title="検出確率と必要な試行回数">
性質 $\varphi$ の生成分布 $\mu$ のもとでの失敗率を $\theta \in [0, 1]$ とし、$X_1, X_2, \ldots$ を分布 $\mu$ に従う独立な入力とする。$N \ge 1$ について、$X_1, \ldots, X_N$ の中に少なくとも 1 つ反例がある事象を $D_N$ とする。

1. $P(D_N) = 1 - (1 - \theta)^N \ge 1 - e^{-\theta N}$。
2. $0 \lt \delta \lt 1$、$\theta \gt 0$ とする。$N \ge \ln(1/\delta)/\theta$ ならば $P(D_N) \ge 1 - \delta$。
3. $0 \lt \delta \lt 1$、$\theta \gt 0$ とする。$N \lt (1 - \delta)/\theta$ ならば $P(D_N) \lt 1 - \delta$。
4. $0 \lt \theta \lt 1$ とする。最初の反例が現れる番号を $\tau$ とすると、$P(\tau = k) = (1 - \theta)^{k-1}\theta$（$k = 1, 2, \ldots$）で、$E[\tau] = 1/\theta$。
</Theorem>

この定理は、「反例が出る確率は試すほど 1 に近づく」ことを式にしたものです。(2) は「これだけ試せば十分」という上からの目安、(3) は「これより少ないと足りない」という下からの目安で、両方そろって初めて必要な回数が $1/\theta$ の程度だと言えます。証明は、硬貨を $N$ 回投げて一度も表が出ない確率を考えるのと同じ計算です。

<Proof of="thm-detection-probability">
(1) 反例が 1 つも出ない確率が $(1 - \theta)^N$ で、$(1 - \theta)^N \le e^{-\theta N}$ であることは、無作為な反例探索についての定理（<Ref to="computer-science/research-computing/verification-of-computations#thm-random-search-bound" /> の 1）です。$D_N$ はその余事象なので、$P(D_N) = 1 - (1 - \theta)^N \ge 1 - e^{-\theta N}$ です。

(2) $\theta N \ge \ln(1/\delta)$ なので $e^{-\theta N} \le e^{-\ln(1/\delta)} = \delta$。(1) より $P(D_N) \ge 1 - \delta$ です。

(3) どの $N$ についても $(1 - \theta)^N \ge 1 - N\theta$ が成り立ちます（<Ref to="computer-science/research-computing/verification-of-computations#thm-random-search-bound" /> の 3）。よって $P(D_N) = 1 - (1 - \theta)^N \le N\theta$ で、$N\theta \lt 1 - \delta$ ならば $P(D_N) \lt 1 - \delta$ です。

(4) $\tau = k$ は「$X_1, \ldots, X_{k-1}$ が反例でなく、$X_k$ が反例である」という事象です。各 $X_i$ が反例である確率は $\theta$ で、$X_1, \ldots, X_k$ は独立なので（<Ref to="mathematics/probability/random-variables#def-independence" />）、確率は $(1 - \theta)^{k-1}\theta$ です。これは成功確率 $\theta$ の幾何分布（<Ref to="mathematics/hs-probability/distributions-and-inference#def-geometric-distribution" />）で、その期待値は $1/\theta$ です（<Ref to="mathematics/hs-probability/distributions-and-inference#thm-geometric-distribution" /> の 3）。
</Proof>

(2) と (3) は、必要な試行回数が $1/\theta$ の定数倍であることを両側から言っています。$\theta = 10^{-3}$、$\delta = 0.01$ なら、$N \ge \ln(100)/10^{-3} \approx 4606$ 個で十分、$N \lt 0.99 \times 10^3 = 990$ 個では不十分です。多くの道具の既定値は 100 個程度なので、既定のままで確実に見つかるのは、失敗率が数 % 以上の誤りです。

**反例が出なかったときに言えること。** $N$ 個試して反例が出なかったとします。(1) から、もし $\theta \gt \ln(1/\delta)/N$ だったなら、そういう結果になる確率は $\delta$ より小さかったはずです。したがって「$\theta \le \ln(1/\delta)/N$ である」と、危険率 $\delta$ で主張できます。$N = 100$、$\delta = 0.05$ なら $\theta \le 0.03$ です。言えるのはここまでです。**性質が成り立つ（$\theta = 0$）とは言えません。** しかもこの $\theta$ は、テストに使った生成分布での失敗率で、実際の利用者の入力の分布での失敗率ではありません。

<Example id="ex-detection-trials" title="検出に要した試行回数">
失敗率 $\theta$ の人工的な性質（一様乱数が $\theta$ 未満なら「反例」）について、最初の反例までの試行回数を 500 回ずつ測ります。

```python
# Python 3.12.14（標準ライブラリのみ）。乱数種は 20261008
import math
import random
import statistics

def trials_until_failure(theta, rng):
    """失敗率 theta の性質を、最初の反例が出るまで調べた回数"""
    n = 1
    while rng.random() >= theta:      # 確率 theta で「反例」
        n += 1
    return n

rng = random.Random(20261008)
print(" theta     1/theta   標本平均   標準誤差   (平均 - 1/theta)/標準誤差   N <= ln(100)/theta の割合")
for theta in (1e-2, 1e-3):
    xs = [trials_until_failure(theta, rng) for _ in range(500)]
    mean = statistics.fmean(xs)
    se = statistics.stdev(xs) / math.sqrt(len(xs))
    n99 = math.log(100) / theta
    frac = sum(x <= n99 for x in xs) / len(xs)
    print(f"{theta:6.0e} {1 / theta:10.1f} {mean:10.1f} {se:10.1f} {(mean - 1 / theta) / se:18.2f} {frac:28.3f}")
```

```text
 theta     1/theta   標本平均   標準誤差   (平均 - 1/theta)/標準誤差   N <= ln(100)/theta の割合
 1e-02      100.0       98.4        4.3              -0.37                        0.994
 1e-03     1000.0     1037.7       49.8               0.76                        0.986
```

標本平均は $1/\theta$ から標準誤差の 1 倍以内にあり、<Ref to="thm-detection-probability" /> (4) と整合しています。最後の列は、$\ln(100)/\theta$ 回以内に反例が見つかった割合で、(2) の保証 $0.99$ の前後の値です（500 回の標本での割合なので、$0.99$ のまわりに標準誤差 $\sqrt{0.99 \times 0.01/500} \approx 0.004$ ほどばらつきます）。
</Example>

### 3.2. 境界値を混ぜる

「整数を一様に生成する」と決めたとします。64 ビットの符号つき整数は $2^{64}$ 個あり、一様に選んで $0$ を引く確率は $2^{-64} \approx 5.4 \times 10^{-20}$ です。$x = 0$ でだけ破れる性質（ゼロ除算）は、<Ref to="thm-detection-probability" /> (3) により、$10^{17}$ 個試しても見つかる確率が $10^{17} \times 2^{-64} \approx 0.005$ 以下です。ところが実際の誤りは、$0$、$\pm 1$、最大値・最小値、空の列といった特別な値に集中します。前章の境界値分析（<Ref to="computer-science/software-design-testing/testing-theory#thm-boundary-fault-model" />）が狙ったのもそこでした。

<Proposition id="prop-generator-coverage" title="特殊値を混ぜた生成分布の失敗率">
$\mu_0$ を $X$ 上の確率分布、$B \subseteq X$ を $b \ge 1$ 個の元からなる有限集合（境界値・特殊値の集合）、$\nu$ を $B$ 上の一様分布、$0 \lt w \le 1$ とする。**混合分布** $\mu = (1 - w)\mu_0 + w\nu$（確率 $w$ で $B$ から一様に、確率 $1 - w$ で $\mu_0$ から選ぶ）のもとで、反例の集合 $F$ が $B$ の元を少なくとも 1 つ含むならば、失敗率は
$$
\theta = \mu(F) \ge \frac{w}{b}
$$
を満たす。したがって $N \ge b \ln(1/\delta)/w$ 個の独立な入力で、確率 $1 - \delta$ 以上で反例が見つかる。
</Proposition>

<Proof of="prop-generator-coverage">
$x^{*} \in F \cap B$ をとります。$\mu(F) = (1 - w)\mu_0(F) + w\nu(F) \ge w\nu(F) \ge w\nu(\{x^{*}\}) = w/b$ です（$\mu_0(F) \ge 0$、$\{x^{*}\} \subseteq F$、$\nu$ は $b$ 点の上の一様分布）。後半は、$\ln(1/\delta)/\theta \le b\ln(1/\delta)/w \le N$ なので <Ref to="thm-detection-probability" /> (2) から従います。
</Proof>

$w = 0.1$、$b = 10$ とすると $\theta \ge 0.01$ で、$\delta = 0.01$ に対して $N \ge 461$ で足ります。一様な生成での $2^{-64}$ と比べると、$17$ 桁以上の違いです。払う代償は、残りの入力に使える試行が $1 - w$ 倍に減ることだけです。実際の道具の整数の生成器が一様でなく、小さい値や境界の値を出しやすく作られているのはこのためです。

この命題も仮定つきです。保証されるのは、反例の集合が**用意した特殊値を含む**ときだけです。「$x = 12345$ のときだけ誤る」実装は、$12345$ を $B$ に入れていなければ、やはり見つかりません。どの値を特殊値とみなすかは、人が（前章の同値分割と境界値分析を使って）決めることです。

## 4. 再帰的なデータの生成器の大きさ

木・式・入れ子のリストのような再帰的なデータの生成器は、「確率 $p$ で子をもつ節点を作り、子を同じ生成器で再帰的に作る」と書くのが自然です。$p$ の選び方を誤ると、生成が終わらなかったり、巨大なデータばかりできたりします。

<Theorem id="thm-recursive-generator-size" title="再帰的な生成器の停止と大きさ">
$0 \lt p \lt 1$ とする。$0$ と $1$ からなる有限の文字列（空の文字列 $\varepsilon$ を含む）の全体を $\{0, 1\}^{*}$ とし、確率空間の上に、独立な確率変数の族 $(\xi_u)_{u \in \{0, 1\}^{*}}$ で $P(\xi_u = 1) = p$、$P(\xi_u = 0) = 1 - p$ を満たすものが与えられているとする。文字列 $u$ のすべての真の接頭辞 $v$ について $\xi_v = 1$ であるとき、$u$ は**生成される**といい、生成される文字列の全体を $\mathcal{T}$ とする（$\varepsilon$ は根で、つねに生成される。生成された $u$ は、$\xi_u = 1$ なら 2 つの子 $u0$、$u1$ をもつ節点、$\xi_u = 0$ なら葉である）。長さ $j$ の生成される文字列の個数を $Z_j$、木の大きさを $S = \sum_{j \ge 0} Z_j \in \{1, 2, \ldots\} \cup \{\infty\}$ とする。

1. $E[Z_j] = (2p)^j$。したがって $p \lt 1/2$ ならば $E[S] = \dfrac{1}{1 - 2p}$、$p \ge 1/2$ ならば $E[S] = \infty$。
2. $P(S \lt \infty) = \min\Bigl(1, \dfrac{1 - p}{p}\Bigr)$。すなわち $p \le 1/2$ ならば確率 $1$ で生成は止まり、$p \gt 1/2$ ならば止まらない確率が $\dfrac{2p - 1}{p} \gt 0$ である。
3. $p \lt 1/2$ のとき、任意の $a \gt 0$ について $P(S \ge a) \le \dfrac{1}{(1 - 2p)\,a}$。
4. 深さ $d$ で打ち切る（長さ $d$ の文字列は必ず葉にする）と、大きさはつねに $2^{d+1} - 1$ 以下である。
</Theorem>

(1) は大きさの平均、(2) は「そもそも止まるか」を述べています。この 2 つは別の性質で、確率 $1$ で止まっても平均の大きさが無限ということがあります。証明の (2) は少し長いので、方針を先に述べます。深さ $d + 1$ に節点が 1 つもない確率 $q_d$ を考えると、根が葉であるか、根の 2 つの子のそれぞれから始まる部分木がどちらも深さ $d$ 以内で終わるか、のどちらかなので、$q_d$ の次の値は今の値から決まります（漸化式）。その極限が止まる確率で、極限は漸化式の不動点として求めます。

<Proof of="thm-recursive-generator-size">
(1) 長さ $j$ の文字列 $u$ の真の接頭辞は、長さ $0, 1, \ldots, j - 1$ の $j$ 個です。$u$ が生成されるのはその $j$ 個の $\xi_v$ がすべて $1$ のときで、独立性（<Ref to="mathematics/probability/random-variables#def-independence" />）から確率は $p^j$ です。$Z_j$ は、長さ $j$ の $2^j$ 個の文字列についての「生成される」の指示関数の和なので、期待値の線形性（<Ref to="mathematics/probability/random-variables#def-expectation" /> から従います）により $E[Z_j] = 2^j p^j = (2p)^j$ です。

$S_J = \sum_{j=0}^{J} Z_j$ は $J$ について広義単調増加な非負の確率変数の列で、$S$ に各点で収束します。単調収束定理（<Ref to="mathematics/probability/random-variables#thm-mct" />）により
$$
E[S] = \lim_{J \to \infty} E[S_J] = \lim_{J \to \infty} \sum_{j=0}^{J} (2p)^j
$$
です。$2p \lt 1$ ならば等比級数の和（<Ref to="mathematics/calculus/series-and-convergence#prop-geometric-series" />）で $1/(1 - 2p)$。$2p \ge 1$ ならば各項が $1$ 以上なので部分和は $J + 1$ 以上で、極限は $\infty$ です。

(2) $d \ge 0$ について、事象 $A_d = \{Z_{d+1} = 0\}$（深さ $d + 1$ に節点がない）を考え、$q_d = P(A_d)$ とおきます。

**$\{S \lt \infty\} = \bigcup_d A_d$ であること。** 生成される文字列の真の接頭辞は生成されるので（接頭辞の接頭辞はまた接頭辞です）、$Z_{d+1} = 0$ ならば長さ $d + 2$ 以上の文字列も生成されません。よって $A_d \subseteq A_{d+1}$ で、$A_d$ の上では $\mathcal{T}$ は長さ $d$ 以下の文字列からなり、$S \le 1 + 2 + \cdots + 2^d = 2^{d+1} - 1 \lt \infty$ です。逆に $S \lt \infty$ なら、$\mathcal{T}$ は有限集合なので、その元の長さの最大値を $d$ とすれば $Z_{d+1} = 0$ です。$A_0 \subseteq A_1 \subseteq \cdots$ なので、確率の下からの連続性（<Ref to="mathematics/probability/probability-spaces#thm-continuity" /> の 1）により $P(S \lt \infty) = \lim_{d \to \infty} q_d$ です。

**漸化式 $q_0 = 1 - p$、$q_{d+1} = (1 - p) + p\,q_d^2$。** $Z_1 = 0$ は $\xi_\varepsilon = 0$ と同値なので $q_0 = 1 - p$ です。長さ $d + 2$ の文字列は $u = iw$（$i \in \{0, 1\}$、$w$ は長さ $d + 1$）と書け、その真の接頭辞は $\varepsilon$ と、$w$ の真の接頭辞 $w'$ に対する $iw'$ です。したがって $u$ が生成されるのは、$\xi_\varepsilon = 1$ かつ「$w$ のすべての真の接頭辞 $w'$ について $\xi_{iw'} = 1$」のときです。$i \in \{0, 1\}$ について、事象 $B^i_d$ を「長さ $d + 1$ のどの $w$ についても、$\xi_{iw'} = 1$ がすべての真の接頭辞 $w'$ で成り立つことはない」と定めると、
$$
A_{d+1} = \{\xi_\varepsilon = 0\} \cup \bigl(\{\xi_\varepsilon = 1\} \cap B^0_d \cap B^1_d\bigr)
$$
で、右辺の 2 つの事象は交わりません。3 つの事象 $\{\xi_\varepsilon = 1\}$、$B^0_d$、$B^1_d$ は、それぞれ $\xi_\varepsilon$、$(\xi_{0w'})_{|w'| \le d}$、$(\xi_{1w'})_{|w'| \le d}$ という、互いに重ならない有限個の変数の組の値だけで決まります。有限個の独立な $0/1$ 変数の値の組（配置）の確率は、各変数の確率の積なので、3 つの事象の共通部分の確率は、3 組の配置についての和が積に分かれて、$P(\xi_\varepsilon = 1)\,P(B^0_d)\,P(B^1_d)$ になります。さらに、$B^i_d$ が $(\xi_{iw'})$ の配置で決まる仕方は、$A_d$ が $(\xi_{w'})_{|w'| \le d}$ の配置で決まる仕方と同じで（$A_d$ は「長さ $d + 1$ のどの $w$ についても、$\xi_{w'} = 1$ がすべての真の接頭辞 $w'$ で成り立つことはない」です）、配置の確率も同じ形の積なので、$P(B^i_d) = P(A_d) = q_d$ です。以上から $q_{d+1} = (1 - p) + p\,q_d^2$ です。

**極限。** $(q_d)$ は広義単調増加で $1$ 以下なので収束し、極限を $q$ とします。$g(x) = (1 - p) + px^2$ は連続なので、漸化式の両辺の極限をとって $q = g(q)$、すなわち $pq^2 - q + (1 - p) = 0$ です。左辺は
$$
pq^2 - q + (1 - p) = (q - 1)\bigl(pq - (1 - p)\bigr)
$$
と因数分解できる（右辺を展開すると $pq^2 - (1 - p)q - pq + (1 - p) = pq^2 - q + (1 - p)$）ので、$q = 1$ または $q = r$、ここで $r = (1 - p)/p$ です。

$p \le 1/2$ のとき $r \ge 1$ で、$q \le 1$ なので、$q = 1$ です（$r = 1$ の場合も含めて）。

$p \gt 1/2$ のとき $r \lt 1$ です。すべての $d$ で $q_d \le r$ であることを帰納法（<Ref to="mathematics/foundations/proof-techniques#thm-induction" />）で示します。$q_0 = 1 - p \le (1 - p)/p = r$（$p \le 1$ より）。$q_d \le r$ とすると、$g$ は $x \ge 0$ で単調増加なので $q_{d+1} = g(q_d) \le g(r) = r$ です。よって $q \le r \lt 1$ で、$q$ は $1$ でないので $q = r$ です。止まらない確率は $1 - r = (2p - 1)/p$ です。

(3) $S$ は非負で、(1) より $E[S] = 1/(1 - 2p)$ なので、マルコフの不等式（<Ref to="mathematics/probability/random-variables#thm-markov" />）から $P(S \ge a) \le E[S]/a$ です。

(4) 長さ $d$ の文字列を必ず葉にすると、生成される文字列の長さは $d$ 以下です。長さ $j$ の文字列は $2^j$ 個なので、大きさは $\sum_{j=0}^{d} 2^j = 2^{d+1} - 1$ 以下です。
</Proof>

$p = 1/2$ は、もっとも素朴な書き方（「硬貨を投げて、表なら子を 2 つ作る」）にあたります。このとき生成は確率 $1$ で止まりますが、大きさの期待値は無限です。**ときどき、とてつもなく大きい木ができます。** テストがたまに極端に遅くなる、メモリを使い果たす、という症状の原因になります。安全なのは、(4) のように深さや大きさの上限で打ち切るか、深さとともに $p$ を小さくする設計です。<Ref to="ex-json-roundtrip" /> の `st.recursive(..., max_leaves=10)` は、葉の数に上限を置いています。

$q = (1 - p) + pq^2$ は、「根が葉であるか、根が子を 2 つもち両方の部分木が有限であるか」という場合分けを式にしたもので、分枝過程の絶滅確率（ここでは、生成がいつか止まる確率）の方程式として知られています。

次の実験では、(a) で定理の (1) の平均を、(b) で打ち切らずに止まらない確率を確かめます。$p = 1/2$ の行では、上限を上げると打ち切られる割合が減る（確率 $1$ で止まる、(2)）一方で平均は増え続ける（期待値が無限、(1)）という、2 つの別の性質が同時に現れています。

<Example id="ex-recursive-generator-size" title="生成された木の大きさ">
```python
# Python 3.12.14（標準ライブラリのみ）。乱数種は 20261008
import math
import random
import statistics

def tree_size(p, rng, cap):
    """各節点が確率 p で 2 つの子をもつ木を生成し、節点数を返す。節点数が cap を超えたら打ち切って cap + 1 を返す。"""
    pending, size = 1, 0             # pending: これから生成する節点の数
    while pending and size <= cap:
        size += 1
        pending -= 1
        if rng.random() < p:
            pending += 2
    return size

rng = random.Random(20261008)
print("(a) p < 1/2: 20000 回の標本平均と 1/(1-2p)")
print("    p  1/(1-2p)  標本平均  標準誤差  (平均-理論)/標準誤差  最大")
for p in (0.30, 0.40, 0.45):
    sizes = [tree_size(p, rng, 10**7) for _ in range(20000)]
    assert max(sizes) <= 10**7                      # 打ち切りは起きていない
    mean, theory = statistics.fmean(sizes), 1 / (1 - 2 * p)
    se = statistics.stdev(sizes) / math.sqrt(len(sizes))
    print(f"{p:5.2f} {theory:9.2f} {mean:9.2f} {se:9.2f} {(mean - theory) / se:16.2f} {max(sizes):9d}")

print("(b) p >= 1/2: 上限 cap で打ち切る。5000 回のうち打ち切られた割合と、min(大きさ, cap+1) の標本平均")
print("    p     cap  打ち切りの割合  (2p-1)/p   標本平均")
for p in (0.50, 0.60):
    for cap in (100, 1000, 10000):
        sizes = [tree_size(p, rng, cap) for _ in range(5000)]
        cut = sum(s > cap for s in sizes) / len(sizes)
        print(f"{p:5.2f} {cap:7d} {cut:12.4f} {max(0.0, (2 * p - 1) / p):12.4f} {statistics.fmean(sizes):10.1f}")
```

```text
(a) p < 1/2: 20000 回の標本平均と 1/(1-2p)
    p  1/(1-2p)  標本平均  標準誤差  (平均-理論)/標準誤差  最大
 0.30      2.50      2.52      0.03             0.74        77
 0.40      5.00      5.10      0.08             1.16       365
 0.45     10.00      9.95      0.22            -0.23       729
(b) p >= 1/2: 上限 cap で打ち切る。5000 回のうち打ち切られた割合と、min(大きさ, cap+1) の標本平均
    p     cap  打ち切りの割合  (2p-1)/p   標本平均
 0.50     100       0.0842       0.0000       15.5
 0.50    1000       0.0294       0.0000       55.5
 0.50   10000       0.0056       0.0000      157.6
 0.60     100       0.3416       0.3333       37.6
 0.60    1000       0.3292       0.3333      332.7
 0.60   10000       0.3248       0.3333     3251.6
```

(a) $p \lt 1/2$ では、標本平均は $1/(1 - 2p)$ から標準誤差の 1.2 倍以内です。平均が $10$ でも、最大は $729$ に達しています。(b) $p = 0.5$ では、上限を 10 倍にするたびに打ち切られる割合は減っていきます（$0$ に向かう。確率 $1$ で止まることに対応）が、打ち切った大きさの平均は増え続けます（期待値が無限であることに対応）。$p = 0.6$ では、打ち切られる割合が上限を上げても $1/3$ の近くにとどまります。これが止まらない確率 $(2p - 1)/p = 1/3$ です（5000 回の標本での標準誤差は約 $0.007$）。
</Example>

## 5. 反例を小さくする：縮約と差分デバッグ

無作為に見つかった反例は、たいてい大きくて、誤りに関係のない部分をたくさん含みます。長さ 37 のリストで性質が破れたと言われても、原因は分かりません。<Ref to="ex-sort-properties" /> で報告された `[0, 0]` のように、小さくて、どの部分も欠かせない反例があれば、原因はほぼ自明です。

### 5.1. 貪欲な縮約

<Definition id="def-shrinking" title="縮約">
$X$ を入力の集合、$\varphi$ を性質とする。**縮約関数**とは、各 $x \in X$ に $X$ の元の有限の列 $\mathrm{shr}(x)$（**縮約の候補**）を対応させる写像をいう。反例 $x_0$ から始める**貪欲な縮約**とは、次の手続きをいう: $x_i$ の候補 $\mathrm{shr}(x_i)$ を列の順に調べ、最初に見つかった反例を $x_{i+1}$ として繰り返す。候補の中に反例がなければ $x_i$ を返して止まる。

反例 $x$ が**局所的に最小**であるとは、$\mathrm{shr}(x)$ の中に反例がないことをいう。写像 $m : X \to \{0, 1, 2, \ldots\}$ が、すべての $x$ とすべての候補 $y \in \mathrm{shr}(x)$ について $m(y) \lt m(x)$ を満たすとき、$m$ を縮約の**尺度**という。
</Definition>

整数なら「$0$」「半分」「絶対値を $1$ 減らしたもの」、リストなら「要素を 1 つ取り除いたもの」「要素の 1 つを縮約したもの」が典型的な候補です。尺度は、整数なら絶対値、リストなら「長さと要素の絶対値の和」などにとれます。

<Theorem id="thm-shrinking-termination" title="縮約の停止性と局所最小性">
縮約関数 $\mathrm{shr}$ が尺度 $m$ をもつとする。反例 $x_0$ から始める貪欲な縮約は、高々 $m(x_0)$ 回の移動のあとで止まり、返される $x$ は局所的に最小な反例である。
</Theorem>

<Proof of="thm-shrinking-termination">
手続きが作る列 $x_0, x_1, \ldots$ は、定義から、すべて反例で、$x_{i+1} \in \mathrm{shr}(x_i)$ です。尺度の条件から $m(x_{i+1}) \lt m(x_i)$ です。

列が無限に続くと仮定します。集合 $\{m(x_i) + 1 \mid i \ge 0\}$ は $\mathbb{N}$ の空でない部分集合なので、整列性（<Ref to="mathematics/foundations/proof-techniques#ax-well-ordering" />）により最小元 $m(x_k) + 1$ をもちます。ところが $m(x_{k+1}) + 1 \lt m(x_k) + 1$ で、最小性に反します。よって列は有限で、手続きは止まります。

移動の回数。$m(x_i) \le m(x_0) - i$ であることが、$i$ についての帰納法（<Ref to="mathematics/foundations/proof-techniques#thm-induction" />）で分かります（$i = 0$ は等号。$m(x_{i+1}) \lt m(x_i)$ で整数値なので $m(x_{i+1}) \le m(x_i) - 1 \le m(x_0) - (i + 1)$）。$m(x_i) \ge 0$ なので $i \le m(x_0)$ です。

止まるのは、$\mathrm{shr}(x_i)$ の中に反例がないときだけです。そのとき返される $x_i$ は反例で、定義により局所的に最小です。
</Proof>

これは、ループ変量による停止性の証明（<Ref to="computer-science/software-design-testing/contracts-and-invariants#thm-total-correctness" />）と同じ議論です。尺度が縮約のループの変量になっています。

尺度のない縮約関数は、止まらないことがあります。整数について $\mathrm{shr}(x) = (-x)$（符号を反転したものを唯一の候補にする）とし、性質を「$x = 0$」とします。反例 $x_0 = 5$ から、$-5$ は反例、その候補 $5$ も反例で、$5, -5, 5, -5, \ldots$ と永久に続きます。「負の数は対応する正の数に縮約する」という規則を入れたいなら、$\mathrm{shr}(x) = (-x)$ を $x \lt 0$ のときに限れば、尺度 $m(x) = 2|x| + [x \lt 0]$ が真に減ります。

<Proposition id="prop-shrink-not-global" title="貪欲な縮約は大域的な最小を保証しない">
尺度をもつ縮約関数と性質であって、貪欲な縮約の結果が、(1) 尺度が最小の反例にならず、(2) 候補を調べる順序によって異なるものが存在する。
</Proposition>

<Proof of="prop-shrink-not-global">
$X = \{0, 1, 2, \ldots\}$、反例の集合を $F = \{4, 6, 11, 12\}$（性質は「$x \notin F$」）、尺度を $m(x) = x$ とします。縮約の候補は、$x \ge 1$ について $\lfloor x/2 \rfloor$ と $x - 1$ の 2 つ（どちらも $x$ より小さい）、$x = 0$ については候補なしとします。$x_0 = 12$ から始めます。

候補を $(\lfloor x/2 \rfloor,\ x - 1)$ の順に調べる場合。$12$ の候補は $6, 11$ で、最初の $6$ が反例なので $6$ に移ります。$6$ の候補は $3, 5$ で、どちらも反例でないので、$6$ を返します。

候補を $(x - 1,\ \lfloor x/2 \rfloor)$ の順に調べる場合。$12$ の候補は $11, 6$ で、最初の $11$ が反例なので $11$ に移ります。$11$ の候補は $10, 5$ で、どちらも反例でないので、$11$ を返します。

結果は $6$ と $11$ で、順序によって異なります。どちらも局所的に最小ですが、尺度が最小の反例は $4$ で、どちらの順序でも到達しません。
</Proof>

<Figure caption="命題の例で、12 から始めた縮約の行き先。候補を調べる順序によって 6 と 11 に分かれ、尺度が最小の反例 4 にはどちらからも届かない。">
<svg viewBox="0 0 600 240" width="100%" role="img" aria-label="反例 12 から、順序 A では 6、順序 B では 11 に移って止まる様子と、どちらからも届かない 4 を示す図">
  <defs>
    <marker id="shr-arrow" viewBox="0 0 10 10" refX="9" refY="5" markerWidth="7" markerHeight="7" orient="auto-start-reverse">
      <path d="M 0 0 L 10 5 L 0 10 z" fill="currentColor" />
    </marker>
  </defs>
  <g fill="none" stroke="currentColor" stroke-width="1.5">
    <circle cx="300" cy="35" r="20" />
    <circle cx="140" cy="125" r="20" />
    <circle cx="460" cy="125" r="20" />
    <circle cx="300" cy="190" r="20" stroke-dasharray="4 3" />
    <line x1="287" y1="52" x2="153" y2="108" marker-end="url(#shr-arrow)" />
    <line x1="313" y1="52" x2="447" y2="108" marker-end="url(#shr-arrow)" />
  </g>
  <g fill="currentColor" font-size="14" text-anchor="middle">
    <text x="300" y="40">12</text>
    <text x="140" y="130">6</text>
    <text x="460" y="130">11</text>
    <text x="300" y="195">4</text>
    <text x="175" y="68">順序 A（半分を先に）</text>
    <text x="425" y="68">順序 B（1 減らす候補を先に）</text>
    <text x="140" y="165">ここで止まる</text>
    <text x="460" y="165">ここで止まる</text>
    <text x="300" y="222" font-size="12">尺度が最小の反例（どちらからも届かない）</text>
  </g>
</svg>
</Figure>

したがって、縮約の結果を「最小の反例」と呼ぶのは正確ではありません。保証されるのは局所最小性です。また、候補の順序が結果を変えるので、縮約を含むテスト全体を**決定的**にしておかないと、同じ誤りに対して実行のたびに違う反例が報告され、原因の調査や、修正の前後の比較が難しくなります（第 8 節）。

### 5.2. 差分デバッグ ddmin

入力が $n$ 個の要素の列（ファイルの行、操作の列、設定の変更の集まり）で、その部分列でテストを実行できるとします。A. Zeller と R. Hildebrandt の **ddmin** は、失敗する入力から、失敗を保つ小さな部分列を系統的に探す算法です。「要素を 1 つずつ取り除く」縮約は $n$ 回の実行で $1$ 個しか減らせませんが、ddmin はまず大きな塊で取り除くことを試み、だめなら塊を細かくしていきます。

<Figure caption="ddmin の粒度。まず 2 つの塊に分けて、塊そのものと、塊を除いた残り（補集合）を試す。どれも失敗しなければ塊の数を倍にする。">
<svg viewBox="0 0 600 150" width="100%" role="img" aria-label="長さ 8 の列を 2 個、4 個、8 個の塊に分けていく ddmin の粒度の図">
  <g fill="currentColor" font-size="13">
    <text x="0" y="33">粒度 2</text>
    <text x="0" y="78">粒度 4</text>
    <text x="0" y="123">粒度 8</text>
  </g>
  <g fill="none" stroke="currentColor" stroke-width="1.5">
    <rect x="70" y="15" width="250" height="28" />
    <rect x="330" y="15" width="250" height="28" />
    <rect x="70" y="60" width="120" height="28" />
    <rect x="200" y="60" width="120" height="28" />
    <rect x="330" y="60" width="120" height="28" />
    <rect x="460" y="60" width="120" height="28" />
    <rect x="70" y="105" width="55" height="28" />
    <rect x="135" y="105" width="55" height="28" />
    <rect x="200" y="105" width="55" height="28" />
    <rect x="265" y="105" width="55" height="28" />
    <rect x="330" y="105" width="55" height="28" />
    <rect x="395" y="105" width="55" height="28" />
    <rect x="460" y="105" width="55" height="28" />
    <rect x="525" y="105" width="55" height="28" />
  </g>
</svg>
</Figure>

次の定義の場合分けを、小さな例で先に追っておきます。長さ 8 の列 $[1, \ldots, 8]$ で、要素 $3$ を含む部分列だけが失敗するとします。粒度 $2$ で $[1, 2, 3, 4]$ と $[5, 6, 7, 8]$ に分け、前者が失敗するので (a) で前者に移ります。次に $[1, 2]$ と $[3, 4]$ に分け、後者が失敗するので $[3, 4]$ に移ります。最後に $[3]$ と $[4]$ に分け、$[3]$ が失敗して終わります。実行は $1 + 2 + 1 = 4$ 回です。塊が失敗しないときに補集合を試す (b) と、細かく分け直す (c) は、原因が離れた 2 要素のようなときに働きます。

<Definition id="def-ddmin" title="ddmin と 1-最小性">
$c$ を相異なる要素の列、$\mathrm{fails}$ を $c$ の部分列に対して「テストが失敗する」かどうかを答える述語とし、$\mathrm{fails}(c)$ は真、空の列については偽とする。失敗する部分列 $c'$ が **1-最小**であるとは、$c'$ からどの 1 要素を取り除いた列も失敗しないことをいう。

**ddmin** は、現在の列 $c$（最初は入力全体）と粒度 $g$（最初は $2$）をもち、$c$ の長さが $2$ 以上のあいだ次を繰り返す。$c$ を、長さがほぼ等しい $g$ 個の連続した塊 $\Delta_1, \ldots, \Delta_g$ に分ける（$\Delta_i$ は $c$ の $\lfloor |c|(i-1)/g \rfloor$ 番目から $\lfloor |c| i/g \rfloor$ 番目の手前まで）。

- (a) ある $\Delta_i$ が失敗するなら、最初のそれを新しい $c$ とし、$g = 2$ とする。
- (b) そうでなく、ある補集合 $c \setminus \Delta_i$ が失敗するなら、最初のそれを新しい $c$ とし、$g$ を $\max(g - 1, 2)$ にする。
- (c) そうでなく、$g \lt |c|$ なら、$g$ を $\min(|c|, 2g)$ にする。
- (d) そうでなければ（$g \ge |c|$）、繰り返しをやめる。

最後の $c$ を返す。
</Definition>

<Theorem id="thm-ddmin" title="ddmin の正しさと実行回数">
$c$ を相異なる $n \ge 1$ 個の要素の列とし、$\mathrm{fails}(c)$ は真、空の列については偽とする。

1. ddmin は止まり、$c$ の部分列で、失敗し、1-最小であるものを返す。
2. $\mathrm{fails}$ の実行回数は $6n^2$ より小さい。
3. 失敗の原因が 1 要素である（ある要素 $e$ があって、$\mathrm{fails}(s)$ が「$e$ が $s$ に含まれる」と同値である）ならば、ddmin は $e$ だけからなる列を返し、実行回数は高々 $2\lceil \log_2 n \rceil$ である。
</Theorem>

<Proof of="thm-ddmin">
$n = 1$ のときは繰り返しが一度も実行されず、$c$ 自身が返ります。$c$ は失敗し、1 要素を除くと空の列で失敗しないので 1-最小、実行回数は $0$ です。以下 $n \ge 2$ とします。

**不変条件。** 繰り返しの先頭で、次が成り立つことを示します: (I1) 現在の $c$ は元の列の部分列で、空でなく、$\mathrm{fails}(c)$ は真。(I2) $|c| \ge 2$ ならば $2 \le g \le |c|$。

最初は $c$ が元の列、$g = 2 \le n$ なので成り立ちます。繰り返しの 1 回で保たれることを見ます。(I2) より $|c|/g \ge 1$ なので、$\lfloor |c| i/g \rfloor \ge \lfloor |c|(i-1)/g \rfloor + 1$ で、どの塊 $\Delta_i$ も空でありません。(a) では、新しい $c$ は失敗した塊 $\Delta_i$ で、空でなく、$g = 2$。新しい $c$ の長さが $2$ 以上なら (I2) が成り立ちます。(b) では、新しい $c$ は失敗した補集合で、$\Delta_i$ 以外の $g - 1 \ge 1$ 個の塊（どれも空でない）を含むので、長さは $g - 1$ 以上です。$g \ge 3$ なら新しい粒度 $g - 1$ は新しい長さ以下で、$g = 2$ なら新しい粒度は $2$ で、新しい長さが $2$ 以上のとき (I2) が成り立ちます。(c) では $c$ は変わらず、新しい粒度は $\min(|c|, 2g)$ で、$g$ より大きく $|c|$ 以下です。

**実行回数 (2) と停止性。** 繰り返しの 1 回は、塊を高々 $g$ 個、補集合を高々 $g$ 個試すので、$\mathrm{fails}$ を高々 $2g$ 回実行します。同じ $c$ のまま続く繰り返しのまとまりを**相**と呼びます。1 つの相の中の粒度を順に $g_1, g_2, \ldots, g_r$、$|c| = \ell$ とします。相の中で次の繰り返しに進むのは (c) のときだけなので、$i \lt r$ について $g_i \lt \ell$ かつ $g_{i+1} = \min(\ell, 2g_i)$ です。$i \le r - 2$ なら $g_{i+1} \lt \ell$ なので $g_{i+1} = 2g_i$、すなわち $g_i = g_{i+1}/2$ です。よって $j = 0, 1, \ldots, r - 2$ について $g_{r-1-j} = g_{r-1}/2^j \lt \ell/2^j$ で、
$$
\sum_{i=1}^{r} g_i \lt \ell\Bigl(1 + \frac12 + \frac14 + \cdots\Bigr) + g_r \le 2\ell + \ell = 3\ell
$$
です（$g_r \le \ell$ は (I2)）。とくに $r$ は有限で、1 つの相の実行回数は $2 \cdot 3\ell = 6\ell \le 6n$ より小さい。相が終わるのは、(a) か (b) で $c$ が真に短い列（塊は $g \ge 2$ 個ありどれも空でないので、塊も補集合も $c$ より短い）に置き換わるときか、(d) で止まるときです。$c$ の長さは相ごとに真に減り、相があるのは長さが $2$ 以上 $n$ 以下のときなので、相は高々 $n - 1$ 個です。したがって手続きは止まり、実行回数は $6n(n - 1) \lt 6n^2$ より小さい。

**1-最小性 (1)。** 返される $c$ は (I1) により元の列の部分列で、失敗します。止まり方は 2 通りです。$|c| = 1$ で止まったなら、1 要素を除いた列は空で、仮定により失敗しません。(d) で止まったなら、(I2) と $g \ge |c|$ から $g = |c|$ で、$g$ 個の空でない塊の長さの和が $g$ なので、どの塊もちょうど 1 要素です。その回の (b) の検査で、補集合 $c \setminus \Delta_i$、すなわち $c$ から 1 要素を除いた列はどれも失敗しなかったので、$c$ は 1-最小です。

**原因が 1 要素の場合 (3)。** (I1) より $\mathrm{fails}(c)$ は真なので、現在の $c$ はつねに $e$ を含みます。粒度がつねに $2$ であることを示します。最初は $2$ です。$g = 2$ のとき、2 つの塊のうち $e$ を含むほうが失敗するので、(a) が適用され、$g = 2$ のままです。この回の実行は、塊を順に試して高々 $2$ 回です。新しい $c$ はその塊で、長さは $\lceil \ell/2 \rceil$ 以下です。$\ell$ が偶数なら $\lceil \ell/2 \rceil - 1 = \ell/2 - 1 \le (\ell - 1)/2$、奇数なら $\lceil \ell/2 \rceil - 1 = (\ell - 1)/2$ なので、$t$ 回の繰り返しのあとの長さ $\ell_t$ は $\ell_t - 1 \le (n - 1)/2^t$ を満たします。$t = \lceil \log_2 n \rceil$ とすると $2^t \ge n \gt n - 1$ なので $\ell_t - 1 \lt 1$、すなわち $\ell_t = 1$ です。よって繰り返しは高々 $\lceil \log_2 n \rceil$ 回、実行は高々 $2\lceil \log_2 n \rceil$ 回で、返される列は $e$ を含む長さ $1$ の列です。
</Proof>

(3) は二分探索です。「半分に分けて、失敗するほうを残す」ことを繰り返すので、回数は $\log_2 n$ の程度になります（<Ref to="computer-science/algorithms/searching#thm-binary-cost" /> と同じ数え方）。(2) の $6n^2$ は、塊で取り除くことにことごとく失敗し、最後に 1 要素ずつ取り除くしかない場合の評価です。実際の入力はその中間にあります。

<Example id="ex-ddmin-runs" title="ddmin の実装と実行回数">
<Ref to="def-ddmin" /> をそのまま書いたものです。

```python
# Python 3.12.14（標準ライブラリのみ）
def ddmin(c, fails):
    """失敗する列 c から 1-最小な失敗部分列を求める。fails(s) は部分列 s でテストが失敗するとき True。
    返り値は (結果, テストの実行回数)。"""
    runs = 0
    def test(s):
        nonlocal runs
        runs += 1
        return fails(s)
    n = 2                                      # 粒度（分割の個数）
    while len(c) >= 2:
        size = len(c)
        cuts = [size * i // n for i in range(n + 1)]
        chunks = [c[cuts[i]:cuts[i + 1]] for i in range(n)]
        complements = [c[:cuts[i]] + c[cuts[i + 1]:] for i in range(n)]
        for d in chunks:                       # (a) 部分への縮小
            if test(d):
                c, n = d, 2
                break
        else:
            for d in complements:              # (b) 補集合への縮小
                if test(d):
                    c, n = d, max(n - 1, 2)
                    break
            else:
                if n >= size:                  # (d) これ以上細かくできない
                    break
                n = min(size, 2 * n)           # (c) 粒度を倍にする
    return c, runs

if __name__ == "__main__":
    c = list(range(64))
    evens = set(range(0, 64, 2))
    cases = [("原因が 1 要素 {37}", lambda s: 37 in s),
             ("原因が 2 要素 {20, 21}", lambda s: 20 in s and 21 in s),
             ("原因が 2 要素 {5, 60}", lambda s: 5 in s and 60 in s),
             ("偶数の 32 要素がすべて必要", lambda s: evens <= set(s)),
             ("64 要素がすべて必要", lambda s: len(s) == 64)]
    for name, fails in cases:
        result, runs = ddmin(c, fails)
        shown = result if len(result) <= 4 else f"(長さ {len(result)})"
        print(f"{name}: 結果 {shown}, 実行回数 {runs}")

    two_minimal = lambda s: {2, 3, 4} <= set(s) or {1, 5} <= set(s)
    print("極小な失敗集合が 2 つ:", ddmin(list(range(1, 9)), two_minimal))
    nonmono = lambda s: s == [1, 2, 3, 4] or s == [1, 3]
    print("単調でないテスト:", ddmin([1, 2, 3, 4], nonmono))
```

```text
原因が 1 要素 {37}: 結果 [37], 実行回数 9
原因が 2 要素 {20, 21}: 結果 [20, 21], 実行回数 11
原因が 2 要素 {5, 60}: 結果 [5, 60], 実行回数 79
偶数の 32 要素がすべて必要: 結果 (長さ 32), 実行回数 2300
64 要素がすべて必要: 結果 (長さ 64), 実行回数 252
極小な失敗集合が 2 つ: ([2, 3, 4], 16)
単調でないテスト: ([1, 2, 3, 4], 12)
```

長さ $n = 64$ の入力についての結果を、定理と照らします。

- 原因が 1 要素なら $9$ 回で、<Ref to="thm-ddmin" /> (3) の上界 $2\lceil \log_2 64 \rceil = 12$ 回以内です。1 要素ずつ取り除く方法なら $63$ 回かかります。
- 原因が 2 要素でも、2 つが隣り合っていれば（同じ塊に入るので）$11$ 回です。離れていると、どちらの半分も単独では失敗しないので粒度を上げることになり、$79$ 回に増えます。
- 偶数番目の $32$ 要素がすべて必要な場合は $2300$ 回で、$n^2 = 4096$ の程度です。奇数番目の要素を、最大の粒度で 1 つずつ取り除くことになります。これが (2) の $n^2$ に比例する場合です。上界 $6n^2 = 24576$ には余裕があります。
- $64$ 要素がすべて必要な場合は、一度も縮小できず、粒度 $2, 4, \ldots, 64$ で $2 \times (2 + 4 + \cdots + 64) = 252$ 回試して終わります。

最後の 2 行は、1-最小が「最小」でないことの例です。「$\{2, 3, 4\}$ を含むか、$\{1, 5\}$ を含むと失敗」というテストは**単調**（失敗する列を含む列は失敗する）ですが、ddmin は前半 $[1, 2, 3, 4]$ が失敗するのを見てそちらに進み、要素数 $3$ の $[2, 3, 4]$ を返します。要素数が最小の失敗集合 $\{1, 5\}$ は見つかりません。単調でないテスト（$[1, 2, 3, 4]$ と $[1, 3]$ だけが失敗する。要素 $2$ と $4$ が、そろっているときだけ互いの影響を打ち消すような状況）では、ddmin は $[1, 2, 3, 4]$ をそのまま返します。どの 1 要素を除いても失敗しないので 1-最小ですが、2 要素を除いた $[1, 3]$ は失敗します。1-最小性は「1 つ取り除く」という操作についての局所最小性で、<Ref to="prop-shrink-not-global" /> と同じ限界をもちます。
</Example>

## 6. 正しい出力が分からないとき：変成関係

数値計算、機械学習のモデル、コンパイラ、検索エンジンのように、個々の入力に対する正しい出力を人が用意できないプログラムがあります（オラクル問題。<Ref to="computer-science/software-design-testing/testing-theory#prop-oracle-problem" />）。そのようなときでも、**入力をこう変えたら、出力はこう変わるはずだ**という関係なら分かることがあります。

<Definition id="def-metamorphic" title="変成関係">
$f : X \to Y$ を（正しい）関数とする。写像 $g : X \to X$ と $h : Y \to Y$ の組 $(g, h)$ が、すべての $x \in X$ について
$$
f(g(x)) = h(f(x))
$$
を満たすとき、$(g, h)$ を $f$ の**変成関係**という。$f$ の実装 $\tilde f : X \to Y$ に対する、入力 $x$ での $(g, h)$ の**検査**とは、$\tilde f(g(x)) = h(\tilde f(x))$ を確かめることをいう。
</Definition>

検査に $f$ の値は現れません。$\tilde f$ を 2 回実行して、結果どうしを比べるだけです。整列なら $g$ は入力の並べ替え、$h$ は恒等写像（並べ替えても結果は同じ）。$\sin$ なら $g(x) = \pi - x$、$h$ は恒等写像（$\sin(\pi - x) = \sin x$）や、$g(x) = -x$、$h(y) = -y$（奇関数）です。

<Theorem id="thm-metamorphic-detection" title="変成関係の検査が検出できる誤り">
$f : X \to Y$ を関数、$\mathcal{R}$ を $f$ の変成関係の集合とする。写像 $\tilde f : X \to Y$ のうち、$\mathcal{R}$ のすべての関係をすべての入力で満たすものの全体を
$$
U(\mathcal{R}) = \{\, \tilde f \mid \text{すべての } (g, h) \in \mathcal{R} \text{ と } x \in X \text{ について } \tilde f(g(x)) = h(\tilde f(x)) \,\}
$$
とおく。

1. $f \in U(\mathcal{R})$ である。実装 $\tilde f$ について、$\mathcal{R}$ の検査がある関係とある入力で不合格になることは、$\tilde f \notin U(\mathcal{R})$ と同値である。とくに $\tilde f \in U(\mathcal{R})$ ならば、$\tilde f \ne f$ であっても、検査の入力をどう選んでも誤りは検出されない。
2. $\mathcal{R} \subseteq \mathcal{R}'$ ならば $U(\mathcal{R}') \subseteq U(\mathcal{R})$ で、$U(\mathcal{R} \cup \mathcal{R}') = U(\mathcal{R}) \cap U(\mathcal{R}')$ である。
3. 写像 $c : Y \to Y$ が $\mathcal{R}$ のすべての $(g, h)$ について $c \circ h = h \circ c$ を満たすならば、$c \circ f \in U(\mathcal{R})$ である。写像 $k : X \to X$ が $\mathcal{R}$ のすべての $(g, h)$ について $k \circ g = g \circ k$ を満たすならば、$f \circ k \in U(\mathcal{R})$ である。
</Theorem>

<Proof of="thm-metamorphic-detection">
(1) $f \in U(\mathcal{R})$ は変成関係の定義そのものです。検査が $(g, h) \in \mathcal{R}$ と $x$ で不合格になるとは $\tilde f(g(x)) \ne h(\tilde f(x))$ のことで、そのような $(g, h)$ と $x$ が存在することは、$U(\mathcal{R})$ の定義の否定、すなわち $\tilde f \notin U(\mathcal{R})$ です。

(2) $\tilde f \in U(\mathcal{R}')$ なら、$\mathcal{R}'$ のすべての関係を満たすので、その一部である $\mathcal{R}$ の関係もすべて満たし、$\tilde f \in U(\mathcal{R})$ です。$\tilde f$ が $\mathcal{R} \cup \mathcal{R}'$ のすべての関係を満たすことは、$\mathcal{R}$ のすべてと $\mathcal{R}'$ のすべてを満たすことと同じなので、後半が成り立ちます。

(3) $(g, h) \in \mathcal{R}$、$x \in X$ とします。$f(g(x)) = h(f(x))$ なので
$$
(c \circ f)(g(x)) = c\bigl(h(f(x))\bigr) = h\bigl(c(f(x))\bigr) = h\bigl((c \circ f)(x)\bigr)
$$
です（2 つ目の等号が $c \circ h = h \circ c$）。同様に
$$
(f \circ k)(g(x)) = f\bigl(g(k(x))\bigr) = h\bigl(f(k(x))\bigr) = h\bigl((f \circ k)(x)\bigr)
$$
です（1 つ目の等号が $k \circ g = g \circ k$、2 つ目が $x$ の代わりに $k(x)$ での変成関係）。
</Proof>

この定理が何のためにあるかを補足します。変成関係の検査は正しい出力を使わないので、関係を満たしてしまう誤った実装があれば見逃します。そこで、関係をすべて満たす実装の集合 $U(\mathcal{R})$ を作り、「検査で見分けられない実装はどれか」を調べるのが (1)〜(3) です。

$U(\mathcal{R})$ は、$\mathcal{R}$ の検査が**見分けられない実装**の集合です。(1) は、検出できる誤りがちょうど「$\mathcal{R}$ を破る実装」であることを言っています。これは、数値計算の検算で不変性の検査が検出できる誤りを特徴づけた命題（<Ref to="computer-science/research-computing/verification-of-computations#prop-invariant-test" />。$h$ が恒等写像の場合にあたります）の一般化です。(2) は関係を増やすほど見分けられない実装が減ることを、(3) は、どんな形の誤りが見逃されるかの目安を与えます。$\mathcal{R}$ のどの $h$ も恒等写像なら、どんな $c$ も条件を満たすので、「正しい結果に何か後処理 $c$ をかけてしまう」誤りは、$c$ が何であれ検出されません。

<Example id="ex-metamorphic-sine" title="sin の変成関係と、見逃される実装">
$f = \sin$ について、3 つの変成関係
$$
\sin(\pi - x) = \sin x, \qquad \sin(-x) = -\sin x, \qquad \sin(x + 2\pi) = \sin x
$$
を $\mathcal{R}$ とします。次の実装は、どれも $U(\mathcal{R})$ に属します。

- $\tilde f(x) = 2\sin x$（係数の誤り）。$c(y) = 2y$ は恒等写像とも $y \mapsto -y$ とも可換なので、<Ref to="thm-metamorphic-detection" /> (3) から従います。
- $\tilde f(x) = 0$。同じく $c(y) = 0$ が条件を満たします。
- $\tilde f(x) = \sin 3x$（引数の誤り）。$\sin(3(\pi - x)) = \sin(3\pi - 3x) = \sin(\pi - 3x) = \sin 3x$、$\sin(3(-x)) = -\sin 3x$、$\sin(3(x + 2\pi)) = \sin(3x + 6\pi) = \sin 3x$ と直接確かめられます。

対称性の関係だけでは、$\sin$ を「同じ対称性をもつ別の関数」から区別できません。種類の違う性質を足す必要があります。たとえば、変成関係ではありませんが、小さい $x$ での評価 $|\sin x - x| \le |x|^3/6$ を $x = 0.1$ で検査します。上界は $0.1^3/6 \approx 1.6667 \times 10^{-4}$ です。正しい実装は $\sin 0.1 = 0.0998334\ldots$ で、差は約 $1.6658 \times 10^{-4}$ となり合格します。$2\sin x$ は差が約 $0.0997$、$\sin 3x$ は $\sin 0.3 \approx 0.2955$ で差が約 $0.196$、$0$ は差が $0.1$ で、3 つとも不合格です。**対称性は形を、既知の値や評価は大きさを縛ります。** 関係を増やすと見分けられない実装の集合が $U(\mathcal{R}) \cap U(\mathcal{R}')$ に減る（(2)）のと同じ理由で、独立な種類の性質を組み合わせると、すべてを通り抜ける誤った実装が減ります。
</Example>

## 7. 状態をもつ系：参照モデルとの比較

集合・待ち行列・キャッシュ・データベースのように、状態をもつ系のテストでは、入力は 1 つの値ではなく**操作の列**です。性質は「どんな操作の列についても、実装の返す結果が、単純で明らかに正しい参照モデルの返す結果と一致する」と書けます。これを**モデルベーステスト**といいます。生成器は操作の列を作り、縮約は列から操作を取り除きます。

理論的な根拠は、契約の章の抽象化関数です。次の命題の言う「模倣関係」は、実装の内部の状態を抽象化関数でモデルの状態に読み替えたとき、どの操作のあとでも両者の対応がずれない、という条件のことです。この条件が成り立つかぎり、操作列の結果は実装とモデルで一致します。

<Proposition id="prop-model-based-soundness" title="模倣関係と操作列のテスト">
データ型の実装 $(\mathrm{Rep}, \mathrm{Init}, (\mathrm{op}_m))$ と、参照モデル（抽象仕様）$(A, a_0, (\mathrm{pre}^A_m), (\mathrm{op}^A_m))$ が与えられているとする（記号は <Ref to="computer-science/software-design-testing/contracts-and-invariants#def-rep-invariant" /> と <Ref to="computer-science/software-design-testing/contracts-and-invariants#prop-abstraction-function" /> のもの）。表現不変条件 $\mathrm{Inv}$ と抽象化関数 $\alpha : \mathrm{Inv} \to A$ の組であって、<Ref to="computer-science/software-design-testing/contracts-and-invariants#prop-abstraction-function" /> の（初期値）と（可換性）を満たすものを、実装とモデルのあいだの**模倣関係**と呼ぶ。

1. 模倣関係が存在するならば、モデルの側で事前条件を満たすどんな操作の列についても、実装の返す結果の列はモデルの返す結果の列と一致する。
2. ある操作の列（モデルの側で事前条件を満たすもの）で、実装の結果とモデルの結果が食い違うならば、模倣関係は存在しない。すなわち、（初期値）を満たすどんな $(\mathrm{Inv}, \alpha)$ についても、（可換性）がどこかで破れている。
</Proposition>

<Proof of="prop-model-based-soundness">
(1) は <Ref to="computer-science/software-design-testing/contracts-and-invariants#prop-abstraction-function" /> の結論（$y_i = y^A_i$）そのものです。(2) は (1) の対偶です。模倣関係が存在すれば結果は一致するので、食い違う列があるなら模倣関係は存在しません。模倣関係とは（初期値）と（可換性）の両方を満たす組のことなので、（初期値）を満たす組は（可換性）を満たしません。
</Proof>

(2) が、テストで不一致が出たときに言えることです。「実装が悪い」とは限りません。モデルが誤っていることも、仕様の理解が食い違っていることもあります（<Ref to="ex-json-roundtrip" /> と同じです）。(1) の逆、「調べた操作の列で一致したから模倣関係がある」は成り立ちません。有限個の列のテストは、ほかの列について何も言いません（<Ref to="computer-science/software-design-testing/testing-theory#thm-testing-incompleteness" />）。

<Example id="ex-heap-model" title="優先度つき待ち行列のモデルベーステスト">
二分ヒープによる優先度つき待ち行列を、「整列済みのリスト」という参照モデルと比べます。`pop` に、子の比較を左の子だけで済ませる誤りを入れてあります。

```python
# test_heap.py — Python 3.12.14 / pytest 9.1.1 / hypothesis 6.168.5
from hypothesis import given, settings, strategies as st

class Heap:
    """二分ヒープによる優先度つき待ち行列。pop は最小の要素を取り出す。"""
    def __init__(self):
        self.a = []
    def push(self, x):
        a = self.a
        a.append(x)
        i = len(a) - 1
        while i > 0 and a[(i - 1) // 2] > a[i]:
            a[(i - 1) // 2], a[i] = a[i], a[(i - 1) // 2]
            i = (i - 1) // 2
    def pop(self):
        a = self.a
        top, last = a[0], a.pop()
        if a:
            a[0] = last
            i = 0
            while 2 * i + 1 < len(a):
                j = 2 * i + 1                     # 誤り: 右の子 2i + 2 と比べて小さいほうを選んでいない
                if a[i] <= a[j]:
                    break
                a[i], a[j] = a[j], a[i]
                i = j
        return top

ops = st.lists(st.one_of(st.tuples(st.just("push"), st.integers()), st.tuples(st.just("pop"))))

@settings(derandomize=True, database=None, max_examples=500)
@given(ops)
def test_heap_agrees_with_model(sequence):
    heap, model = Heap(), []                       # 参照モデル: 整列済みのリスト
    for op in sequence:
        if op[0] == "push":
            heap.push(op[1])
            model.append(op[1])
            model.sort()
        elif model:                                # pop の事前条件: 空でない
            assert heap.pop() == model.pop(0)
```

`pytest test_heap.py -q` の出力の抜粋です。

```text
E               assert 0 == -1
E               Failing test case: test_heap_agrees_with_model(
E                   sequence=[('push', 0),
E                    ('push', -1),
E                    ('push', -1),
E                    ('push', 0),
E                    ('pop',),
E                    ('pop',)],
E               )
1 failed in 1.53s
```

縮約された反例を手で追います。4 回の `push` のあと、配列は $[-1, 0, -1, 0]$ で、ヒープの条件（親は子以下）を満たします。1 回目の `pop` は根の $-1$ を返し、これはモデルと一致します。しかし内部では、末尾の $0$ を根に置いて $[0, 0, -1]$ とし、左の子 $0$ とだけ比べて「$0 \le 0$ なので終わり」としています。根 $0$ が右の子 $-1$ より大きく、**表現不変条件が破れました**。2 回目の `pop` は根の $0$ を返し、モデルの $-1$ と食い違います。

抽象化関数を $\alpha(a) = $「$a$ の要素を昇順に並べたリスト」、不変条件をヒープの条件とすると、1 回目の `pop` のあとの表現は不変条件を満たさず、（可換性）の「$r' \in \mathrm{Inv}$」がここで破れています。結果の食い違いとして見えるのは、その 1 操作あとです。前々章の <Ref to="computer-science/software-design-testing/contracts-and-invariants#ex-representation-leak" /> と同じく、**不変条件が壊れる時点と、症状が出る時点は離れます**。各操作のあとに不変条件を表明で検査すれば（オラクルを強めれば）、1 操作早く、より短い操作列で見つかります。

この反例は 6 操作で、誤りが現れるにはこの程度の長さが必要でした（要素が 3 つ以上残る状態で `pop` し、右の子のほうが小さい必要があります）。人が例示で書くテストが `push` 2 回と `pop` 2 回で終わっていれば、この誤りは通ります。
</Example>

## 8. 失敗を再現できるか

無作為なテストには、「昨日は落ちたのに今日は通る」という不安がつきまといます。これは無作為性そのものの問題ではありません。

<Proposition id="prop-flaky-property-test" title="種による再現">
性質ベーステストの 1 回の実行が、擬似乱数生成器（<Ref to="computer-science/research-computing/reproducible-experiments#def-prng" />）の出力列を受け取る「乱数を消費する決定的なプログラム」である、すなわち、入力の生成、性質 $\varphi$ の評価、縮約、結果（合格か、報告する反例は何か）の出力が、受け取った乱数の値と初期状態だけで決まるとする。このとき、実行の結果は種だけで決まる。とくに、失敗した実行は、同じ種で実行し直せば、同じ反例とともに再現される。
</Proposition>

<Proof of="prop-flaky-property-test">
仮定により、テストの実行は <Ref to="computer-science/research-computing/reproducible-experiments#def-prng" /> の意味での乱数を消費する決定的なプログラムで、止まるものです。その出力が初期状態と種だけで決まることは、種による決定性の命題（<Ref to="computer-science/research-computing/reproducible-experiments#prop-seed-determinism" /> の 2）です。同じプログラムを同じ種で実行すれば、同じ出力、すなわち同じ合否と同じ反例が得られます。
</Proof>

実務上の要点は、**失敗したときに種を記録し、種を指定して実行し直せるようにしておく**ことです。Hypothesis は、見つけた反例を保存して次回の実行で最初に試し、種を指定して実行する手段（`@seed`、`derandomize`）も備えています。この記事の例で `derandomize=True`、`database=None` としたのは、記事の出力を固定するためです。

命題の仮定が破れると、種を固定しても再現しません。破れ方は主に 3 つです。

- **性質の評価が入力以外に依存する。** 現在時刻、乱数（テスト対象の内部で別の生成器を使う）、外部のサービス、ファイルシステムの状態。
- **並行性。** スレッドの切り替わりの順序は種で決まりません。乱数の消費の順序が実行ごとに変わると、同じ種でも別の入力が生成されます（<Ref to="computer-science/research-computing/reproducible-experiments#prop-seed-determinism" /> の 3）。
- **走査の順序。** 集合や辞書の走査の順序に依存するコード。Python では、文字列のハッシュ値がプロセスごとに変わるので、文字列の集合の走査の順序は実行ごとに変わりえます。

3 つ目を確かめます。文字列のハッシュの種を決める環境変数 `PYTHONHASHSEED` を 1、2、1、2 の順に変えて、同じ 1 行のプログラムを 4 回実行します（Python 3.12.14）。

```bash
for h in 1 2 1 2; do PYTHONHASHSEED=$h python -c "print(list({'apple', 'banana', 'cherry'}))"; done
```

```text
['cherry', 'apple', 'banana']
['apple', 'banana', 'cherry']
['cherry', 'apple', 'banana']
['apple', 'banana', 'cherry']
```

ハッシュの種が同じなら順序は同じで、違えば変わります。「集合の最初の要素」に依存する性質は、テストの乱数種を固定しても、この環境変数を固定しなければ再現しません。同じコードで合否が変わる[不安定なテスト](/computer-science/software-design-testing/continuous-integration#def-flaky-test)の確率的な扱いは、継続的インテグレーションの章の主題です。

<Remark id="rem-pbt-literature" title="この記事で扱わなかったこと">
**小さい入力の全数検査。** 無作為に作る代わりに、大きさが一定以下の入力をすべて列挙して調べる方法があります（C. Runciman らの SmallCheck、2008 年）。「誤りの多くは小さい反例をもつ」という経験則（D. Jackson の小スコープ仮説）に基づき、大きさの上限までは反例がないことを保証できます。

**被覆に導かれる fuzzing。** 入力を無作為に変異させ、新しい分岐を通った入力を残して次の変異の元にする方法です。生成分布を、実行の網羅の情報で適応的に変えていることになり、<Ref to="thm-detection-probability" /> の「独立で同じ分布」という仮定の外にあります。

**内部表現の縮約。** Hypothesis は、生成された値そのものではなく、値を作るのに使った乱数の列のほうを縮約します。型ごとに縮約関数を書かなくてよく、生成器の制約（「昇順のリスト」など）を保ったまま縮約できます。D. MacIver と A. Donaldson の 2020 年の論文に説明があります。
</Remark>

## 9. 演習

<Exercise id="exr-sample-size" difficulty="易">
ある性質の失敗率が $\theta = 0.002$ であるとする。

1. 確率 $0.95$ 以上で反例を見つけるのに十分な試行回数を、<Ref to="thm-detection-probability" /> (2) から求めよ。また $1 - (1 - \theta)^N \ge 0.95$ を満たす最小の $N$ を求めよ。
2. 反例の集合が特殊値を 1 つ含むとし、$8$ 個の特殊値を重み $w = 0.2$ で混ぜた生成分布に変える。十分な試行回数はいくつになるか。
<Solution>
1. $\delta = 0.05$ で、$\ln(1/\delta)/\theta = \ln 20 / 0.002 = 2.9957\ldots / 0.002 = 1497.9$ なので、$N \ge 1498$ で十分です。正確には $(0.998)^N \le 0.05$、すなわち $N \ge \ln 0.05 / \ln 0.998 = 2.99573 / 0.00200200 = 1496.4$ なので、最小の $N$ は $1497$ です。(2) の評価は $e^{-\theta} \ge 1 - \theta$ を使っているぶんだけ大きめですが、$\theta$ が小さいのでほとんど差がありません。

2. <Ref to="prop-generator-coverage" /> より $\theta \ge w/b = 0.2/8 = 0.025$ です。$N \ge \ln 20/0.025 = 119.8$ なので、$120$ 個で十分です。$1498$ 個の約 $12$ 分の $1$ です。
</Solution>
</Exercise>

<Exercise id="exr-ternary-generator" difficulty="標準">
各節点が確率 $p$ で 3 つの子をもち、確率 $1 - p$ で葉になる木の生成器を考える（<Ref to="thm-recursive-generator-size" /> の 2 分木を 3 分木に変えたもの）。

1. 大きさの期待値が有限になる $p$ の範囲と、そのときの期待値を求めよ。
2. $p = 1/2$ のとき、生成が止まる確率を求めよ。
<Solution>
1. 深さ $j$ の位置は $3^j$ 個あり、それぞれが生成される確率は $p^j$ なので、$E[Z_j] = (3p)^j$ です。定理の (1) と同じく、$E[S] = \sum_j (3p)^j$ で、$p \lt 1/3$ のとき $1/(1 - 3p)$、$p \ge 1/3$ のとき無限です。

2. 定理の (2) の証明と同じ議論で、深さ $d + 1$ に節点がない確率 $q_d$ は $q_0 = 1 - p$、$q_{d+1} = (1 - p) + p\,q_d^3$ を満たし（根が葉であるか、根が子を 3 つもち 3 つの部分木がどれも深さ $d$ 以内で終わるか）、止まる確率 $q = \lim q_d$ は $q = (1 - p) + pq^3$ の解です。$g(x) = (1 - p) + px^3$ は $x \ge 0$ で単調増加なので、$[0, 1]$ の中の解 $r$ について、$q_0 = 1 - p \le g(r) = r$ から帰納法で $q_d \le r$ が分かり、$q$ は $[0, 1]$ の中の最小の解です。$p = 1/2$ では $q = \frac12 + \frac12 q^3$、すなわち
$$
q^3 - 2q + 1 = (q - 1)(q^2 + q - 1) = 0
$$
で、解は $q = 1$ と $q = \dfrac{-1 \pm \sqrt{5}}{2}$ です。$[0, 1]$ の中の最小の解は $\dfrac{\sqrt{5} - 1}{2} \approx 0.618$ です。止まる確率は約 $0.618$、止まらない確率は約 $0.382$ です。2 分木では安全側の境界だった $p = 1/2$ が、3 分木ではすでに危険な領域にあります。
</Solution>
</Exercise>

<Exercise id="exr-list-shrink-measure" difficulty="標準">
整数のリスト $xs = (x_1, \ldots, x_\ell)$ の縮約の候補を、(i) 要素を 1 つ取り除いたリスト、(ii) $0$ でない要素 $x_i$ を 1 つ選び、絶対値がより小さい整数に置き換えたリスト、とする。

1. $m(xs) = \sum_{i=1}^{\ell} (|x_i| + 1)$ が尺度であることを示し、貪欲な縮約の移動の回数の上界を述べよ。
2. 性質「要素の和は $100$ 未満」について、$(100)$ と $(50, 50)$ がどちらも局所的に最小な反例であることを示せ。尺度が小さいのはどちらか。
<Solution>
1. (i) で $x_i$ を取り除くと、$m$ は $|x_i| + 1 \ge 1$ だけ減ります。(ii) で $x_i$ を $|x_i'| \lt |x_i|$ である $x_i'$ に置き換えると、$m$ は $|x_i| - |x_i'| \ge 1$ だけ減ります。どちらの候補でも $m$ は真に減り、$m$ は非負整数値なので尺度です。<Ref to="thm-shrinking-termination" /> により、反例 $xs_0$ からの貪欲な縮約は高々 $m(xs_0)$ 回の移動で止まります。

2. $(100)$ の候補は、空のリスト（和 $0$）と、$(x')$ で $|x'| \lt 100$ のもの（和は $99$ 以下）で、どれも和が $100$ 未満なので反例ではありません。$(50, 50)$ の候補は、$(50)$（和 $50$）と、一方を $|x'| \lt 50$ の $x'$ に置き換えたもの（和は $50 + x' \le 99$）で、どれも反例ではありません。よってどちらも局所的に最小です。尺度は $m((100)) = 101$、$m((50, 50)) = 102$ で、$(100)$ のほうが小さい。貪欲な縮約がどちらに着くかは、出発点と候補の順序によります（<Ref to="prop-shrink-not-global" />）。「2 つの要素の一方を減らし他方を増やす」という候補を足せば $(50, 50)$ から抜け出せますが、そのときは尺度が真に減ることを改めて確かめる必要があります。
</Solution>
</Exercise>

<Exercise id="exr-mean-metamorphic" difficulty="標準">
実数のリストの算術平均 $f$ について、変成関係を 3 つ考える: (a) 並べ替えても変わらない、(b) 全要素を 2 倍すると結果も 2 倍になる、(c) 全要素に 1 を足すと結果も 1 増える。次の 4 つの誤った実装のうち、この 3 つの検査で検出されるものはどれか。検出されないものについて、それを検出する関係を 1 つ挙げよ。

- $\tilde f_1$: 中央値を返す。
- $\tilde f_2$: 最小値と最大値の平均を返す。
- $\tilde f_3$: 整数のリストに対して、和を要素数で割った商（切り捨て）を返す。
- $\tilde f_4$: 先頭の要素を返す。
<Solution>
$\tilde f_4$ は (a) で検出されます。$(1, 2)$ と、並べ替えた $(2, 1)$ で、結果が $1$ と $2$ です。

$\tilde f_3$ は (b) で検出されます。$(1, 2)$ では $\lfloor 3/2 \rfloor = 1$ で、その 2 倍は $2$。$(2, 4)$ では $\lfloor 6/2 \rfloor = 3 \ne 2$ です。なお (a) と (c) は満たします（和は並べ替えで変わらず、全要素に $1$ を足すと和が要素数だけ増えて商がちょうど $1$ 増えます）。

$\tilde f_1$ と $\tilde f_2$ は、3 つとも満たすので検出されません。中央値も、最小値と最大値の平均も、並べ替えで変わらず、全要素を 2 倍すれば 2 倍に、$1$ を足せば $1$ 増えます。<Ref to="thm-metamorphic-detection" /> の言葉では、$\tilde f_1, \tilde f_2 \in U(\mathcal{R})$ です。

これらを検出する関係として、たとえば「同じ長さの 2 つのリストをつないだものの平均は、それぞれの平均の平均に等しい」があります。$(0, 0, 9)$ と $(1, 1, 1)$ について、中央値は $0$ と $1$ で、その平均は $0.5$ ですが、つないだ $(0, 0, 9, 1, 1, 1)$ の中央値は $1$ です。最小値と最大値の平均は $4.5$ と $1$ で、その平均は $2.75$ ですが、つないだリストでは $4.5$ です。どちらも不合格になります。(a)〜(c) は「位置と尺度の変換に対する振る舞い」という同じ種類の関係で、平均を、同じ振る舞いをするほかの代表値から区別できません。種類の違う関係（加法性）を足すことで区別できます。
</Solution>
</Exercise>

## 参考文献

1. K. Claessen, J. Hughes, "QuickCheck: A lightweight tool for random testing of Haskell programs", *Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP)*, 2000, 268–279. [doi:10.1145/351240.351266](https://doi.org/10.1145/351240.351266) — 性質ベーステストの原論文。生成器と大きさのパラメータ。
2. A. Zeller, R. Hildebrandt, "Simplifying and isolating failure-inducing input", *IEEE Transactions on Software Engineering* 28 (2002), 183–200. [doi:10.1109/32.988498](https://doi.org/10.1109/32.988498) — 差分デバッグ ddmin と 1-最小性。
3. T. Y. Chen, S. C. Cheung, S. M. Yiu, "Metamorphic testing: A new approach for generating next test cases", Technical Report HKUST-CS98-01, Hong Kong University of Science and Technology, 1998 — 変成テストの提案。
4. D. R. MacIver, A. F. Donaldson, "Test-case reduction via test-case generation: Insights from the Hypothesis reducer", *34th European Conference on Object-Oriented Programming (ECOOP)*, 2020 — 内部表現を縮約する方式。
5. C. Runciman, M. Naylor, F. Lindblad, "SmallCheck and Lazy SmallCheck: Automatic exhaustive testing for small values", *Proceedings of the First ACM SIGPLAN Symposium on Haskell*, 2008 — 小さい入力の全数検査。
6. Hypothesis の公式ドキュメント: [https://hypothesis.readthedocs.io/](https://hypothesis.readthedocs.io/) — 生成器（strategies）、設定、状態をもつ系のテスト。
