コンテンツにスキップ

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

対象読者: 本テーマ第 1〜2 章(契約とテストの網羅基準)を学び、学部の確率(期待値・独立性・幾何分布)を知っている人。Hypothesis などの性質ベーステストの経験は仮定しません。

前提となる記事:テストの理論:網羅基準・同値分割と境界値・突然変異テスト、確率変数と期待値:可測関数としての確率変数、ルベーグ積分としての期待値

生 Markdown

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

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

前章 の結論は 2 つありました。有限のテスト集合は、テストしなかった 1 点で誤る実装を通してしまう(定理 2.2[テストの理論])。そして、どの入力を選ぶかの方法はどれも、誤りについての仮定に支えられている。人が入力を選ぶかぎり、選ぶ人が思いつかなかった場合はテストされません。実装した本人がテストを書くなら、実装で考え落とした場合は、テストでも考え落としている可能性が高い。

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

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

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

定義 2.1(性質と反例)↗

XX を入力の集合とする。性質とは、写像 φ:X→{真,偽}\varphi : X \to \{\text{真}, \text{偽}\} であって、各 xx について φ(x)\varphi(x) の値をプログラムで計算できるものをいう。性質 φ\varphi が主張するのは全称命題「すべての x∈Xx \in X について φ(x)\varphi(x) は真」である。φ(x)\varphi(x) が偽である xx を反例という。

これに対して、入力 x1,…,xrx_1, \ldots, x_r と期待される出力 y1,…,yry_1, \ldots, y_r を人が選び、実装 ff について f(xi)=yif(x_i) = y_i を確かめるテストを例示によるテストという。

性質 φ\varphi は、前章のオラクル(定義 2.1[テストの理論])を入力の関数として書いたものです。実装 ff とオラクル OO に対して φ(x)=[(x,f(x))∈O]\varphi(x) = [(x, f(x)) \in O] とおけば、φ\varphi の反例は ff が不合格になる入力です。違いは、期待値を 1 つずつ書く代わりに、どんな入力にも使える判定を書くところにあります。

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

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

不変量の型は、契約による設計 の事後条件や表現不変条件を、そのまま性質にしたものです。性質ベーステストは、契約を無作為な入力で検査する方法だとも言えます。

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

例 2.2(整列の 3 つの性質と、重複を落とす誤り)

整列(定義 2.1[ソートアルゴリズム])の実装に、重複する要素を落とす誤りを入れます。性質を 3 つ書きます。

# 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 の出力の抜粋です。

..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 の出力(報告される反例、とくに 例 7.2 の操作列)は、コードの先頭に書いた版でのものです。末尾の実行時間は実行のたびに変わります。

例 2.3(直列化の往復)

往復の性質は、書くのが簡単で、見つかる誤りが多い型です。Python の標準ライブラリの json について、「JSON にして戻すと元に戻る」を書きます。

# 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
E Failing test case: test_roundtrip(
E x={0: None},
E )

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

定義 3.1(生成器・生成分布・失敗率)↗

生成器とは、乱数の列から入力の集合 XX の元を作る手続きをいう。生成器が作る入力は XX に値をとる確率変数で、その分布 μ\mu を生成分布という。多くの生成器は大きさのパラメータ ss(列の長さの上限、木の深さの上限、整数の絶対値の上限など)をもち、ss ごとに分布 μs\mu_s が決まる。

性質 φ\varphi の、生成分布 μ\mu のもとでの失敗率を、反例の集合の確率

θ=μ({ x∈X∣φ(x) は偽 })\theta = \mu(\{\, x \in X \mid \varphi(x) \text{ は偽} \,\})

と定める。

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

定理 3.2(検出確率と必要な試行回数)✓

性質 φ\varphi の生成分布 μ\mu のもとでの失敗率を θ∈[0,1]\theta \in [0, 1] とし、X1,X2,…X_1, X_2, \ldots を分布 μ\mu に従う独立な入力とする。N≥1N \ge 1 について、X1,…,XNX_1, \ldots, X_N の中に少なくとも 1 つ反例がある事象を DND_N とする。

  1. P(DN)=1−(1−θ)N≥1−e−θNP(D_N) = 1 - (1 - \theta)^N \ge 1 - e^{-\theta N}。
  2. 0<δ<10 \lt \delta \lt 1、θ>0\theta \gt 0 とする。N≥ln⁡(1/δ)/θN \ge \ln(1/\delta)/\theta ならば P(DN)≥1−δP(D_N) \ge 1 - \delta。
  3. 0<δ<10 \lt \delta \lt 1、θ>0\theta \gt 0 とする。N<(1−δ)/θN \lt (1 - \delta)/\theta ならば P(DN)<1−δP(D_N) \lt 1 - \delta。
  4. 0<θ<10 \lt \theta \lt 1 とする。最初の反例が現れる番号を τ\tau とすると、P(τ=k)=(1−θ)k−1θP(\tau = k) = (1 - \theta)^{k-1}\theta(k=1,2,…k = 1, 2, \ldots)で、E[τ]=1/θE[\tau] = 1/\theta。

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

証明(定理 3.2)

(1) 反例が 1 つも出ない確率が (1−θ)N(1 - \theta)^N で、(1−θ)N≤e−θN(1 - \theta)^N \le e^{-\theta N} であることは、無作為な反例探索についての定理(定理 6.2[検算と検証] の 1)です。DND_N はその余事象なので、P(DN)=1−(1−θ)N≥1−e−θNP(D_N) = 1 - (1 - \theta)^N \ge 1 - e^{-\theta N} です。

(2) θN≥ln⁡(1/δ)\theta N \ge \ln(1/\delta) なので e−θN≤e−ln⁡(1/δ)=δe^{-\theta N} \le e^{-\ln(1/\delta)} = \delta。(1) より P(DN)≥1−δP(D_N) \ge 1 - \delta です。

(3) どの NN についても (1−θ)N≥1−Nθ(1 - \theta)^N \ge 1 - N\theta が成り立ちます(定理 6.2[検算と検証] の 3)。よって P(DN)=1−(1−θ)N≤NθP(D_N) = 1 - (1 - \theta)^N \le N\theta で、Nθ<1−δN\theta \lt 1 - \delta ならば P(DN)<1−δP(D_N) \lt 1 - \delta です。

(4) τ=k\tau = k は「X1,…,Xk−1X_1, \ldots, X_{k-1} が反例でなく、XkX_k が反例である」という事象です。各 XiX_i が反例である確率は θ\theta で、X1,…,XkX_1, \ldots, X_k は独立なので(定義 2.3[確率変数と期待値])、確率は (1−θ)k−1θ(1 - \theta)^{k-1}\theta です。これは成功確率 θ\theta の幾何分布(定義 3.4[確率分布と統計的な推測])で、その期待値は 1/θ1/\theta です(定理 3.5[確率分布と統計的な推測] の 3)。

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

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

例 3.3(検出に要した試行回数)

失敗率 θ\theta の人工的な性質(一様乱数が θ\theta 未満なら「反例」)について、最初の反例までの試行回数を 500 回ずつ測ります。

# 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}")
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/θ1/\theta から標準誤差の 1 倍以内にあり、定理 3.2 (4) と整合しています。最後の列は、ln⁡(100)/θ\ln(100)/\theta 回以内に反例が見つかった割合で、(2) の保証 0.990.99 の前後の値です(500 回の標本での割合なので、0.990.99 のまわりに標準誤差 0.99×0.01/500≈0.004\sqrt{0.99 \times 0.01/500} \approx 0.004 ほどばらつきます)。

「整数を一様に生成する」と決めたとします。64 ビットの符号つき整数は 2642^{64} 個あり、一様に選んで 00 を引く確率は 2−64≈5.4×10−202^{-64} \approx 5.4 \times 10^{-20} です。x=0x = 0 でだけ破れる性質(ゼロ除算)は、定理 3.2 (3) により、101710^{17} 個試しても見つかる確率が 1017×2−64≈0.00510^{17} \times 2^{-64} \approx 0.005 以下です。ところが実際の誤りは、00、±1\pm 1、最大値・最小値、空の列といった特別な値に集中します。前章の境界値分析(定理 4.2[テストの理論])が狙ったのもそこでした。

命題 3.4(特殊値を混ぜた生成分布の失敗率)✓

μ0\mu_0 を XX 上の確率分布、B⊆XB \subseteq X を b≥1b \ge 1 個の元からなる有限集合(境界値・特殊値の集合)、ν\nu を BB 上の一様分布、0<w≤10 \lt w \le 1 とする。混合分布 μ=(1−w)μ0+wν\mu = (1 - w)\mu_0 + w\nu(確率 ww で BB から一様に、確率 1−w1 - w で μ0\mu_0 から選ぶ)のもとで、反例の集合 FF が BB の元を少なくとも 1 つ含むならば、失敗率は

θ=μ(F)≥wb\theta = \mu(F) \ge \frac{w}{b}

を満たす。したがって N≥bln⁡(1/δ)/wN \ge b \ln(1/\delta)/w 個の独立な入力で、確率 1−δ1 - \delta 以上で反例が見つかる。

証明(命題 3.4)

x∗∈F∩Bx^{*} \in F \cap B をとります。μ(F)=(1−w)μ0(F)+wν(F)≥wν(F)≥wν({x∗})=w/b\mu(F) = (1 - w)\mu_0(F) + w\nu(F) \ge w\nu(F) \ge w\nu(\{x^{*}\}) = w/b です(μ0(F)≥0\mu_0(F) \ge 0、{x∗}⊆F\{x^{*}\} \subseteq F、ν\nu は bb 点の上の一様分布)。後半は、ln⁡(1/δ)/θ≤bln⁡(1/δ)/w≤N\ln(1/\delta)/\theta \le b\ln(1/\delta)/w \le N なので 定理 3.2 (2) から従います。

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

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

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

Section titled “4. 再帰的なデータの生成器の大きさ”

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

定理 4.1(再帰的な生成器の停止と大きさ)✓

0<p<10 \lt p \lt 1 とする。00 と 11 からなる有限の文字列(空の文字列 ε\varepsilon を含む)の全体を {0,1}∗\{0, 1\}^{*} とし、確率空間の上に、独立な確率変数の族 (ξu)u∈{0,1}∗(\xi_u)_{u \in \{0, 1\}^{*}} で P(ξu=1)=pP(\xi_u = 1) = p、P(ξu=0)=1−pP(\xi_u = 0) = 1 - p を満たすものが与えられているとする。文字列 uu のすべての真の接頭辞 vv について ξv=1\xi_v = 1 であるとき、uu は生成されるといい、生成される文字列の全体を T\mathcal{T} とする(ε\varepsilon は根で、つねに生成される。生成された uu は、ξu=1\xi_u = 1 なら 2 つの子 u0u0、u1u1 をもつ節点、ξu=0\xi_u = 0 なら葉である)。長さ jj の生成される文字列の個数を ZjZ_j、木の大きさを S=∑j≥0Zj∈{1,2,…}∪{∞}S = \sum_{j \ge 0} Z_j \in \{1, 2, \ldots\} \cup \{\infty\} とする。

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

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

証明(定理 4.1)

(1) 長さ jj の文字列 uu の真の接頭辞は、長さ 0,1,…,j−10, 1, \ldots, j - 1 の jj 個です。uu が生成されるのはその jj 個の ξv\xi_v がすべて 11 のときで、独立性(定義 2.3[確率変数と期待値])から確率は pjp^j です。ZjZ_j は、長さ jj の 2j2^j 個の文字列についての「生成される」の指示関数の和なので、期待値の線形性(定義 4.1[確率変数と期待値] から従います)により E[Zj]=2jpj=(2p)jE[Z_j] = 2^j p^j = (2p)^j です。

SJ=∑j=0JZjS_J = \sum_{j=0}^{J} Z_j は JJ について広義単調増加な非負の確率変数の列で、SS に各点で収束します。単調収束定理(定理 2.1[確率変数と期待値])により

E[S]=lim⁡J→∞E[SJ]=lim⁡J→∞∑j=0J(2p)jE[S] = \lim_{J \to \infty} E[S_J] = \lim_{J \to \infty} \sum_{j=0}^{J} (2p)^j

です。2p<12p \lt 1 ならば等比級数の和(命題 3.6[級数と収束判定])で 1/(1−2p)1/(1 - 2p)。2p≥12p \ge 1 ならば各項が 11 以上なので部分和は J+1J + 1 以上で、極限は ∞\infty です。

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

{S<∞}=⋃dAd\{S \lt \infty\} = \bigcup_d A_d であること。 生成される文字列の真の接頭辞は生成されるので(接頭辞の接頭辞はまた接頭辞です)、Zd+1=0Z_{d+1} = 0 ならば長さ d+2d + 2 以上の文字列も生成されません。よって Ad⊆Ad+1A_d \subseteq A_{d+1} で、AdA_d の上では T\mathcal{T} は長さ dd 以下の文字列からなり、S≤1+2+⋯+2d=2d+1−1<∞S \le 1 + 2 + \cdots + 2^d = 2^{d+1} - 1 \lt \infty です。逆に S<∞S \lt \infty なら、T\mathcal{T} は有限集合なので、その元の長さの最大値を dd とすれば Zd+1=0Z_{d+1} = 0 です。A0⊆A1⊆⋯A_0 \subseteq A_1 \subseteq \cdots なので、確率の下からの連続性(定理 4.3[確率空間とコルモゴロフの公理] の 1)により P(S<∞)=lim⁡d→∞qdP(S \lt \infty) = \lim_{d \to \infty} q_d です。

漸化式 q0=1−pq_0 = 1 - p、qd+1=(1−p)+p qd2q_{d+1} = (1 - p) + p\,q_d^2。 Z1=0Z_1 = 0 は ξε=0\xi_\varepsilon = 0 と同値なので q0=1−pq_0 = 1 - p です。長さ d+2d + 2 の文字列は u=iwu = iw(i∈{0,1}i \in \{0, 1\}、ww は長さ d+1d + 1)と書け、その真の接頭辞は ε\varepsilon と、ww の真の接頭辞 w′w' に対する iw′iw' です。したがって uu が生成されるのは、ξε=1\xi_\varepsilon = 1 かつ「ww のすべての真の接頭辞 w′w' について ξiw′=1\xi_{iw'} = 1」のときです。i∈{0,1}i \in \{0, 1\} について、事象 BdiB^i_d を「長さ d+1d + 1 のどの ww についても、ξiw′=1\xi_{iw'} = 1 がすべての真の接頭辞 w′w' で成り立つことはない」と定めると、

Ad+1={ξε=0}∪({ξε=1}∩Bd0∩Bd1)A_{d+1} = \{\xi_\varepsilon = 0\} \cup \bigl(\{\xi_\varepsilon = 1\} \cap B^0_d \cap B^1_d\bigr)

で、右辺の 2 つの事象は交わりません。3 つの事象 {ξε=1}\{\xi_\varepsilon = 1\}、Bd0B^0_d、Bd1B^1_d は、それぞれ ξε\xi_\varepsilon、(ξ0w′)∣w′∣≤d(\xi_{0w'})_{|w'| \le d}、(ξ1w′)∣w′∣≤d(\xi_{1w'})_{|w'| \le d} という、互いに重ならない有限個の変数の組の値だけで決まります。有限個の独立な 0/10/1 変数の値の組(配置)の確率は、各変数の確率の積なので、3 つの事象の共通部分の確率は、3 組の配置についての和が積に分かれて、P(ξε=1) P(Bd0) P(Bd1)P(\xi_\varepsilon = 1)\,P(B^0_d)\,P(B^1_d) になります。さらに、BdiB^i_d が (ξiw′)(\xi_{iw'}) の配置で決まる仕方は、AdA_d が (ξw′)∣w′∣≤d(\xi_{w'})_{|w'| \le d} の配置で決まる仕方と同じで(AdA_d は「長さ d+1d + 1 のどの ww についても、ξw′=1\xi_{w'} = 1 がすべての真の接頭辞 w′w' で成り立つことはない」です)、配置の確率も同じ形の積なので、P(Bdi)=P(Ad)=qdP(B^i_d) = P(A_d) = q_d です。以上から qd+1=(1−p)+p qd2q_{d+1} = (1 - p) + p\,q_d^2 です。

極限。 (qd)(q_d) は広義単調増加で 11 以下なので収束し、極限を qq とします。g(x)=(1−p)+px2g(x) = (1 - p) + px^2 は連続なので、漸化式の両辺の極限をとって q=g(q)q = g(q)、すなわち pq2−q+(1−p)=0pq^2 - q + (1 - p) = 0 です。左辺は

pq2−q+(1−p)=(q−1)(pq−(1−p))pq^2 - q + (1 - p) = (q - 1)\bigl(pq - (1 - p)\bigr)

と因数分解できる(右辺を展開すると pq2−(1−p)q−pq+(1−p)=pq2−q+(1−p)pq^2 - (1 - p)q - pq + (1 - p) = pq^2 - q + (1 - p))ので、q=1q = 1 または q=rq = r、ここで r=(1−p)/pr = (1 - p)/p です。

p≤1/2p \le 1/2 のとき r≥1r \ge 1 で、q≤1q \le 1 なので、q=1q = 1 です(r=1r = 1 の場合も含めて)。

p>1/2p \gt 1/2 のとき r<1r \lt 1 です。すべての dd で qd≤rq_d \le r であることを帰納法(定理 3.2[証明の技術])で示します。q0=1−p≤(1−p)/p=rq_0 = 1 - p \le (1 - p)/p = r(p≤1p \le 1 より)。qd≤rq_d \le r とすると、gg は x≥0x \ge 0 で単調増加なので qd+1=g(qd)≤g(r)=rq_{d+1} = g(q_d) \le g(r) = r です。よって q≤r<1q \le r \lt 1 で、qq は 11 でないので q=rq = r です。止まらない確率は 1−r=(2p−1)/p1 - r = (2p - 1)/p です。

(3) SS は非負で、(1) より E[S]=1/(1−2p)E[S] = 1/(1 - 2p) なので、マルコフの不等式(定理 6.1[確率変数と期待値])から P(S≥a)≤E[S]/aP(S \ge a) \le E[S]/a です。

(4) 長さ dd の文字列を必ず葉にすると、生成される文字列の長さは dd 以下です。長さ jj の文字列は 2j2^j 個なので、大きさは ∑j=0d2j=2d+1−1\sum_{j=0}^{d} 2^j = 2^{d+1} - 1 以下です。

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

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

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

例 4.2(生成された木の大きさ)

# 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}")
(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<1/2p \lt 1/2 では、標本平均は 1/(1−2p)1/(1 - 2p) から標準誤差の 1.2 倍以内です。平均が 1010 でも、最大は 729729 に達しています。(b) p=0.5p = 0.5 では、上限を 10 倍にするたびに打ち切られる割合は減っていきます(00 に向かう。確率 11 で止まることに対応)が、打ち切った大きさの平均は増え続けます(期待値が無限であることに対応)。p=0.6p = 0.6 では、打ち切られる割合が上限を上げても 1/31/3 の近くにとどまります。これが止まらない確率 (2p−1)/p=1/3(2p - 1)/p = 1/3 です(5000 回の標本での標準誤差は約 0.0070.007)。

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

Section titled “5. 反例を小さくする:縮約と差分デバッグ”

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

定義 5.1(縮約)↗

XX を入力の集合、φ\varphi を性質とする。縮約関数とは、各 x∈Xx \in X に XX の元の有限の列 shr(x)\mathrm{shr}(x)(縮約の候補)を対応させる写像をいう。反例 x0x_0 から始める貪欲な縮約とは、次の手続きをいう: xix_i の候補 shr(xi)\mathrm{shr}(x_i) を列の順に調べ、最初に見つかった反例を xi+1x_{i+1} として繰り返す。候補の中に反例がなければ xix_i を返して止まる。

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

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

定理 5.2(縮約の停止性と局所最小性)✓

縮約関数 shr\mathrm{shr} が尺度 mm をもつとする。反例 x0x_0 から始める貪欲な縮約は、高々 m(x0)m(x_0) 回の移動のあとで止まり、返される xx は局所的に最小な反例である。

証明(定理 5.2)

手続きが作る列 x0,x1,…x_0, x_1, \ldots は、定義から、すべて反例で、xi+1∈shr(xi)x_{i+1} \in \mathrm{shr}(x_i) です。尺度の条件から m(xi+1)<m(xi)m(x_{i+1}) \lt m(x_i) です。

列が無限に続くと仮定します。集合 {m(xi)+1∣i≥0}\{m(x_i) + 1 \mid i \ge 0\} は N\mathbb{N} の空でない部分集合なので、整列性(公理 3.1[証明の技術])により最小元 m(xk)+1m(x_k) + 1 をもちます。ところが m(xk+1)+1<m(xk)+1m(x_{k+1}) + 1 \lt m(x_k) + 1 で、最小性に反します。よって列は有限で、手続きは止まります。

移動の回数。m(xi)≤m(x0)−im(x_i) \le m(x_0) - i であることが、ii についての帰納法(定理 3.2[証明の技術])で分かります(i=0i = 0 は等号。m(xi+1)<m(xi)m(x_{i+1}) \lt m(x_i) で整数値なので m(xi+1)≤m(xi)−1≤m(x0)−(i+1)m(x_{i+1}) \le m(x_i) - 1 \le m(x_0) - (i + 1))。m(xi)≥0m(x_i) \ge 0 なので i≤m(x0)i \le m(x_0) です。

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

これは、ループ変量による停止性の証明(定理 5.2[契約による設計])と同じ議論です。尺度が縮約のループの変量になっています。

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

命題 5.3(貪欲な縮約は大域的な最小を保証しない)✓

尺度をもつ縮約関数と性質であって、貪欲な縮約の結果が、(1) 尺度が最小の反例にならず、(2) 候補を調べる順序によって異なるものが存在する。

証明(命題 5.3)

X={0,1,2,…}X = \{0, 1, 2, \ldots\}、反例の集合を F={4,6,11,12}F = \{4, 6, 11, 12\}(性質は「x∉Fx \notin F」)、尺度を m(x)=xm(x) = x とします。縮約の候補は、x≥1x \ge 1 について ⌊x/2⌋\lfloor x/2 \rfloor と x−1x - 1 の 2 つ(どちらも xx より小さい)、x=0x = 0 については候補なしとします。x0=12x_0 = 12 から始めます。

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

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

結果は 66 と 1111 で、順序によって異なります。どちらも局所的に最小ですが、尺度が最小の反例は 44 で、どちらの順序でも到達しません。

126114順序 A(半分を先に)順序 B(1 減らす候補を先に)ここで止まるここで止まる尺度が最小の反例(どちらからも届かない)
命題の例で、12 から始めた縮約の行き先。候補を調べる順序によって 6 と 11 に分かれ、尺度が最小の反例 4 にはどちらからも届かない。

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

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

粒度 2粒度 4粒度 8
ddmin の粒度。まず 2 つの塊に分けて、塊そのものと、塊を除いた残り(補集合)を試す。どれも失敗しなければ塊の数を倍にする。

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

定義 5.4(ddmin と 1-最小性)↗

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

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

  • (a) ある Δi\Delta_i が失敗するなら、最初のそれを新しい cc とし、g=2g = 2 とする。
  • (b) そうでなく、ある補集合 c∖Δic \setminus \Delta_i が失敗するなら、最初のそれを新しい cc とし、gg を max⁡(g−1,2)\max(g - 1, 2) にする。
  • (c) そうでなく、g<∣c∣g \lt |c| なら、gg を min⁡(∣c∣,2g)\min(|c|, 2g) にする。
  • (d) そうでなければ(g≥∣c∣g \ge |c|)、繰り返しをやめる。

最後の cc を返す。

定理 5.5(ddmin の正しさと実行回数)✓

cc を相異なる n≥1n \ge 1 個の要素の列とし、fails(c)\mathrm{fails}(c) は真、空の列については偽とする。

  1. ddmin は止まり、cc の部分列で、失敗し、1-最小であるものを返す。
  2. fails\mathrm{fails} の実行回数は 6n26n^2 より小さい。
  3. 失敗の原因が 1 要素である(ある要素 ee があって、fails(s)\mathrm{fails}(s) が「ee が ss に含まれる」と同値である)ならば、ddmin は ee だけからなる列を返し、実行回数は高々 2⌈log⁡2n⌉2\lceil \log_2 n \rceil である。
証明(定理 5.5)

n=1n = 1 のときは繰り返しが一度も実行されず、cc 自身が返ります。cc は失敗し、1 要素を除くと空の列で失敗しないので 1-最小、実行回数は 00 です。以下 n≥2n \ge 2 とします。

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

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

実行回数 (2) と停止性。 繰り返しの 1 回は、塊を高々 gg 個、補集合を高々 gg 個試すので、fails\mathrm{fails} を高々 2g2g 回実行します。同じ cc のまま続く繰り返しのまとまりを相と呼びます。1 つの相の中の粒度を順に g1,g2,…,grg_1, g_2, \ldots, g_r、∣c∣=ℓ|c| = \ell とします。相の中で次の繰り返しに進むのは (c) のときだけなので、i<ri \lt r について gi<ℓg_i \lt \ell かつ gi+1=min⁡(ℓ,2gi)g_{i+1} = \min(\ell, 2g_i) です。i≤r−2i \le r - 2 なら gi+1<ℓg_{i+1} \lt \ell なので gi+1=2gig_{i+1} = 2g_i、すなわち gi=gi+1/2g_i = g_{i+1}/2 です。よって j=0,1,…,r−2j = 0, 1, \ldots, r - 2 について gr−1−j=gr−1/2j<ℓ/2jg_{r-1-j} = g_{r-1}/2^j \lt \ell/2^j で、

∑i=1rgi<ℓ(1+12+14+⋯ )+gr≤2ℓ+ℓ=3ℓ\sum_{i=1}^{r} g_i \lt \ell\Bigl(1 + \frac12 + \frac14 + \cdots\Bigr) + g_r \le 2\ell + \ell = 3\ell

です(gr≤ℓg_r \le \ell は (I2))。とくに rr は有限で、1 つの相の実行回数は 2⋅3ℓ=6ℓ≤6n2 \cdot 3\ell = 6\ell \le 6n より小さい。相が終わるのは、(a) か (b) で cc が真に短い列(塊は g≥2g \ge 2 個ありどれも空でないので、塊も補集合も cc より短い)に置き換わるときか、(d) で止まるときです。cc の長さは相ごとに真に減り、相があるのは長さが 22 以上 nn 以下のときなので、相は高々 n−1n - 1 個です。したがって手続きは止まり、実行回数は 6n(n−1)<6n26n(n - 1) \lt 6n^2 より小さい。

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

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

(3) は二分探索です。「半分に分けて、失敗するほうを残す」ことを繰り返すので、回数は log⁡2n\log_2 n の程度になります(定理 3.3[探索アルゴリズム] と同じ数え方)。(2) の 6n26n^2 は、塊で取り除くことにことごとく失敗し、最後に 1 要素ずつ取り除くしかない場合の評価です。実際の入力はその中間にあります。

例 5.6(ddmin の実装と実行回数)

定義 5.4 をそのまま書いたものです。

# 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))
原因が 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=64n = 64 の入力についての結果を、定理と照らします。

  • 原因が 1 要素なら 99 回で、定理 5.5 (3) の上界 2⌈log⁡264⌉=122\lceil \log_2 64 \rceil = 12 回以内です。1 要素ずつ取り除く方法なら 6363 回かかります。
  • 原因が 2 要素でも、2 つが隣り合っていれば(同じ塊に入るので)1111 回です。離れていると、どちらの半分も単独では失敗しないので粒度を上げることになり、7979 回に増えます。
  • 偶数番目の 3232 要素がすべて必要な場合は 23002300 回で、n2=4096n^2 = 4096 の程度です。奇数番目の要素を、最大の粒度で 1 つずつ取り除くことになります。これが (2) の n2n^2 に比例する場合です。上界 6n2=245766n^2 = 24576 には余裕があります。
  • 6464 要素がすべて必要な場合は、一度も縮小できず、粒度 2,4,…,642, 4, \ldots, 64 で 2×(2+4+⋯+64)=2522 \times (2 + 4 + \cdots + 64) = 252 回試して終わります。

最後の 2 行は、1-最小が「最小」でないことの例です。「{2,3,4}\{2, 3, 4\} を含むか、{1,5}\{1, 5\} を含むと失敗」というテストは単調(失敗する列を含む列は失敗する)ですが、ddmin は前半 [1,2,3,4][1, 2, 3, 4] が失敗するのを見てそちらに進み、要素数 33 の [2,3,4][2, 3, 4] を返します。要素数が最小の失敗集合 {1,5}\{1, 5\} は見つかりません。単調でないテスト([1,2,3,4][1, 2, 3, 4] と [1,3][1, 3] だけが失敗する。要素 22 と 44 が、そろっているときだけ互いの影響を打ち消すような状況)では、ddmin は [1,2,3,4][1, 2, 3, 4] をそのまま返します。どの 1 要素を除いても失敗しないので 1-最小ですが、2 要素を除いた [1,3][1, 3] は失敗します。1-最小性は「1 つ取り除く」という操作についての局所最小性で、命題 5.3 と同じ限界をもちます。

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

Section titled “6. 正しい出力が分からないとき:変成関係”

数値計算、機械学習のモデル、コンパイラ、検索エンジンのように、個々の入力に対する正しい出力を人が用意できないプログラムがあります(オラクル問題。命題 2.6[テストの理論])。そのようなときでも、入力をこう変えたら、出力はこう変わるはずだという関係なら分かることがあります。

定義 6.1(変成関係)↗

f:X→Yf : X \to Y を(正しい)関数とする。写像 g:X→Xg : X \to X と h:Y→Yh : Y \to Y の組 (g,h)(g, h) が、すべての x∈Xx \in X について

f(g(x))=h(f(x))f(g(x)) = h(f(x))

を満たすとき、(g,h)(g, h) を ff の変成関係という。ff の実装 f~:X→Y\tilde f : X \to Y に対する、入力 xx での (g,h)(g, h) の検査とは、f~(g(x))=h(f~(x))\tilde f(g(x)) = h(\tilde f(x)) を確かめることをいう。

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

定理 6.2(変成関係の検査が検出できる誤り)✓

f:X→Yf : X \to Y を関数、R\mathcal{R} を ff の変成関係の集合とする。写像 f~:X→Y\tilde f : X \to Y のうち、R\mathcal{R} のすべての関係をすべての入力で満たすものの全体を

U(R)={ f~∣すべての (g,h)∈R と x∈X について f~(g(x))=h(f~(x)) }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∈U(R)f \in U(\mathcal{R}) である。実装 f~\tilde f について、R\mathcal{R} の検査がある関係とある入力で不合格になることは、f~∉U(R)\tilde f \notin U(\mathcal{R}) と同値である。とくに f~∈U(R)\tilde f \in U(\mathcal{R}) ならば、f~≠f\tilde f \ne f であっても、検査の入力をどう選んでも誤りは検出されない。
  2. R⊆R′\mathcal{R} \subseteq \mathcal{R}' ならば U(R′)⊆U(R)U(\mathcal{R}') \subseteq U(\mathcal{R}) で、U(R∪R′)=U(R)∩U(R′)U(\mathcal{R} \cup \mathcal{R}') = U(\mathcal{R}) \cap U(\mathcal{R}') である。
  3. 写像 c:Y→Yc : Y \to Y が R\mathcal{R} のすべての (g,h)(g, h) について c∘h=h∘cc \circ h = h \circ c を満たすならば、c∘f∈U(R)c \circ f \in U(\mathcal{R}) である。写像 k:X→Xk : X \to X が R\mathcal{R} のすべての (g,h)(g, h) について k∘g=g∘kk \circ g = g \circ k を満たすならば、f∘k∈U(R)f \circ k \in U(\mathcal{R}) である。
証明(定理 6.2)

(1) f∈U(R)f \in U(\mathcal{R}) は変成関係の定義そのものです。検査が (g,h)∈R(g, h) \in \mathcal{R} と xx で不合格になるとは f~(g(x))≠h(f~(x))\tilde f(g(x)) \ne h(\tilde f(x)) のことで、そのような (g,h)(g, h) と xx が存在することは、U(R)U(\mathcal{R}) の定義の否定、すなわち f~∉U(R)\tilde f \notin U(\mathcal{R}) です。

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

(3) (g,h)∈R(g, h) \in \mathcal{R}、x∈Xx \in X とします。f(g(x))=h(f(x))f(g(x)) = h(f(x)) なので

(c∘f)(g(x))=c(h(f(x)))=h(c(f(x)))=h((c∘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∘h=h∘cc \circ h = h \circ c)。同様に

(f∘k)(g(x))=f(g(k(x)))=h(f(k(x)))=h((f∘k)(x))(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∘g=g∘kk \circ g = g \circ k、2 つ目が xx の代わりに k(x)k(x) での変成関係)。

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

U(R)U(\mathcal{R}) は、R\mathcal{R} の検査が見分けられない実装の集合です。(1) は、検出できる誤りがちょうど「R\mathcal{R} を破る実装」であることを言っています。これは、数値計算の検算で不変性の検査が検出できる誤りを特徴づけた命題(命題 5.3[検算と検証]。hh が恒等写像の場合にあたります)の一般化です。(2) は関係を増やすほど見分けられない実装が減ることを、(3) は、どんな形の誤りが見逃されるかの目安を与えます。R\mathcal{R} のどの hh も恒等写像なら、どんな cc も条件を満たすので、「正しい結果に何か後処理 cc をかけてしまう」誤りは、cc が何であれ検出されません。

例 6.3(sin の変成関係と、見逃される実装)

f=sin⁡f = \sin について、3 つの変成関係

sin⁡(π−x)=sin⁡x,sin⁡(−x)=−sin⁡x,sin⁡(x+2π)=sin⁡x\sin(\pi - x) = \sin x, \qquad \sin(-x) = -\sin x, \qquad \sin(x + 2\pi) = \sin x

を R\mathcal{R} とします。次の実装は、どれも U(R)U(\mathcal{R}) に属します。

  • f~(x)=2sin⁡x\tilde f(x) = 2\sin x(係数の誤り)。c(y)=2yc(y) = 2y は恒等写像とも y↦−yy \mapsto -y とも可換なので、定理 6.2 (3) から従います。
  • f~(x)=0\tilde f(x) = 0。同じく c(y)=0c(y) = 0 が条件を満たします。
  • f~(x)=sin⁡3x\tilde f(x) = \sin 3x(引数の誤り)。sin⁡(3(π−x))=sin⁡(3π−3x)=sin⁡(π−3x)=sin⁡3x\sin(3(\pi - x)) = \sin(3\pi - 3x) = \sin(\pi - 3x) = \sin 3x、sin⁡(3(−x))=−sin⁡3x\sin(3(-x)) = -\sin 3x、sin⁡(3(x+2π))=sin⁡(3x+6π)=sin⁡3x\sin(3(x + 2\pi)) = \sin(3x + 6\pi) = \sin 3x と直接確かめられます。

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

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

Section titled “7. 状態をもつ系:参照モデルとの比較”

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

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

命題 7.1(模倣関係と操作列のテスト)✓

データ型の実装 (Rep,Init,(opm))(\mathrm{Rep}, \mathrm{Init}, (\mathrm{op}_m)) と、参照モデル(抽象仕様)(A,a0,(premA),(opmA))(A, a_0, (\mathrm{pre}^A_m), (\mathrm{op}^A_m)) が与えられているとする(記号は 定義 6.1[契約による設計] と 命題 6.4[契約による設計] のもの)。表現不変条件 Inv\mathrm{Inv} と抽象化関数 α:Inv→A\alpha : \mathrm{Inv} \to A の組であって、命題 6.4[契約による設計] の(初期値)と(可換性)を満たすものを、実装とモデルのあいだの模倣関係と呼ぶ。

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

(1) は 命題 6.4[契約による設計] の結論(yi=yiAy_i = y^A_i)そのものです。(2) は (1) の対偶です。模倣関係が存在すれば結果は一致するので、食い違う列があるなら模倣関係は存在しません。模倣関係とは(初期値)と(可換性)の両方を満たす組のことなので、(初期値)を満たす組は(可換性)を満たしません。

(2) が、テストで不一致が出たときに言えることです。「実装が悪い」とは限りません。モデルが誤っていることも、仕様の理解が食い違っていることもあります(例 2.3 と同じです)。(1) の逆、「調べた操作の列で一致したから模倣関係がある」は成り立ちません。有限個の列のテストは、ほかの列について何も言いません(定理 2.2[テストの理論])。

例 7.2(優先度つき待ち行列のモデルベーステスト)

二分ヒープによる優先度つき待ち行列を、「整列済みのリスト」という参照モデルと比べます。pop に、子の比較を左の子だけで済ませる誤りを入れてあります。

# 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 の出力の抜粋です。

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, 0, -1, 0] で、ヒープの条件(親は子以下)を満たします。1 回目の pop は根の −1-1 を返し、これはモデルと一致します。しかし内部では、末尾の 00 を根に置いて [0,0,−1][0, 0, -1] とし、左の子 00 とだけ比べて「0≤00 \le 0 なので終わり」としています。根 00 が右の子 −1-1 より大きく、表現不変条件が破れました。2 回目の pop は根の 00 を返し、モデルの −1-1 と食い違います。

抽象化関数を α(a)=\alpha(a) = 「aa の要素を昇順に並べたリスト」、不変条件をヒープの条件とすると、1 回目の pop のあとの表現は不変条件を満たさず、(可換性)の「r′∈Invr' \in \mathrm{Inv}」がここで破れています。結果の食い違いとして見えるのは、その 1 操作あとです。前々章の 例 6.3[契約による設計] と同じく、不変条件が壊れる時点と、症状が出る時点は離れます。各操作のあとに不変条件を表明で検査すれば(オラクルを強めれば)、1 操作早く、より短い操作列で見つかります。

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

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

命題 8.1(種による再現)✓

性質ベーステストの 1 回の実行が、擬似乱数生成器(定義 5.1[再現できる数値実験])の出力列を受け取る「乱数を消費する決定的なプログラム」である、すなわち、入力の生成、性質 φ\varphi の評価、縮約、結果(合格か、報告する反例は何か)の出力が、受け取った乱数の値と初期状態だけで決まるとする。このとき、実行の結果は種だけで決まる。とくに、失敗した実行は、同じ種で実行し直せば、同じ反例とともに再現される。

証明(命題 8.1)

仮定により、テストの実行は 定義 5.1[再現できる数値実験] の意味での乱数を消費する決定的なプログラムで、止まるものです。その出力が初期状態と種だけで決まることは、種による決定性の命題(命題 5.2[再現できる数値実験] の 2)です。同じプログラムを同じ種で実行すれば、同じ出力、すなわち同じ合否と同じ反例が得られます。

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

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

  • 性質の評価が入力以外に依存する。 現在時刻、乱数(テスト対象の内部で別の生成器を使う)、外部のサービス、ファイルシステムの状態。
  • 並行性。 スレッドの切り替わりの順序は種で決まりません。乱数の消費の順序が実行ごとに変わると、同じ種でも別の入力が生成されます(命題 5.2[再現できる数値実験] の 3)。
  • 走査の順序。 集合や辞書の走査の順序に依存するコード。Python では、文字列のハッシュ値がプロセスごとに変わるので、文字列の集合の走査の順序は実行ごとに変わりえます。

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

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

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

注意 8.2(この記事で扱わなかったこと)

小さい入力の全数検査。 無作為に作る代わりに、大きさが一定以下の入力をすべて列挙して調べる方法があります(C. Runciman らの SmallCheck、2008 年)。「誤りの多くは小さい反例をもつ」という経験則(D. Jackson の小スコープ仮説)に基づき、大きさの上限までは反例がないことを保証できます。

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

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

演習 9.1易

ある性質の失敗率が θ=0.002\theta = 0.002 であるとする。

  1. 確率 0.950.95 以上で反例を見つけるのに十分な試行回数を、定理 3.2 (2) から求めよ。また 1−(1−θ)N≥0.951 - (1 - \theta)^N \ge 0.95 を満たす最小の NN を求めよ。
  2. 反例の集合が特殊値を 1 つ含むとし、88 個の特殊値を重み w=0.2w = 0.2 で混ぜた生成分布に変える。十分な試行回数はいくつになるか。
解答
  1. δ=0.05\delta = 0.05 で、ln⁡(1/δ)/θ=ln⁡20/0.002=2.9957…/0.002=1497.9\ln(1/\delta)/\theta = \ln 20 / 0.002 = 2.9957\ldots / 0.002 = 1497.9 なので、N≥1498N \ge 1498 で十分です。正確には (0.998)N≤0.05(0.998)^N \le 0.05、すなわち N≥ln⁡0.05/ln⁡0.998=2.99573/0.00200200=1496.4N \ge \ln 0.05 / \ln 0.998 = 2.99573 / 0.00200200 = 1496.4 なので、最小の NN は 14971497 です。(2) の評価は e−θ≥1−θe^{-\theta} \ge 1 - \theta を使っているぶんだけ大きめですが、θ\theta が小さいのでほとんど差がありません。

  2. 命題 3.4 より θ≥w/b=0.2/8=0.025\theta \ge w/b = 0.2/8 = 0.025 です。N≥ln⁡20/0.025=119.8N \ge \ln 20/0.025 = 119.8 なので、120120 個で十分です。14981498 個の約 1212 分の 11 です。

演習 9.2標準

各節点が確率 pp で 3 つの子をもち、確率 1−p1 - p で葉になる木の生成器を考える(定理 4.1 の 2 分木を 3 分木に変えたもの)。

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

  2. 定理の (2) の証明と同じ議論で、深さ d+1d + 1 に節点がない確率 qdq_d は q0=1−pq_0 = 1 - p、qd+1=(1−p)+p qd3q_{d+1} = (1 - p) + p\,q_d^3 を満たし(根が葉であるか、根が子を 3 つもち 3 つの部分木がどれも深さ dd 以内で終わるか)、止まる確率 q=lim⁡qdq = \lim q_d は q=(1−p)+pq3q = (1 - p) + pq^3 の解です。g(x)=(1−p)+px3g(x) = (1 - p) + px^3 は x≥0x \ge 0 で単調増加なので、[0,1][0, 1] の中の解 rr について、q0=1−p≤g(r)=rq_0 = 1 - p \le g(r) = r から帰納法で qd≤rq_d \le r が分かり、qq は [0,1][0, 1] の中の最小の解です。p=1/2p = 1/2 では q=12+12q3q = \frac12 + \frac12 q^3、すなわち

q3−2q+1=(q−1)(q2+q−1)=0q^3 - 2q + 1 = (q - 1)(q^2 + q - 1) = 0

で、解は q=1q = 1 と q=−1±52q = \dfrac{-1 \pm \sqrt{5}}{2} です。[0,1][0, 1] の中の最小の解は 5−12≈0.618\dfrac{\sqrt{5} - 1}{2} \approx 0.618 です。止まる確率は約 0.6180.618、止まらない確率は約 0.3820.382 です。2 分木では安全側の境界だった p=1/2p = 1/2 が、3 分木ではすでに危険な領域にあります。

演習 9.3標準

整数のリスト xs=(x1,…,xℓ)xs = (x_1, \ldots, x_\ell) の縮約の候補を、(i) 要素を 1 つ取り除いたリスト、(ii) 00 でない要素 xix_i を 1 つ選び、絶対値がより小さい整数に置き換えたリスト、とする。

  1. m(xs)=∑i=1ℓ(∣xi∣+1)m(xs) = \sum_{i=1}^{\ell} (|x_i| + 1) が尺度であることを示し、貪欲な縮約の移動の回数の上界を述べよ。
  2. 性質「要素の和は 100100 未満」について、(100)(100) と (50,50)(50, 50) がどちらも局所的に最小な反例であることを示せ。尺度が小さいのはどちらか。
解答
  1. (i) で xix_i を取り除くと、mm は ∣xi∣+1≥1|x_i| + 1 \ge 1 だけ減ります。(ii) で xix_i を ∣xi′∣<∣xi∣|x_i'| \lt |x_i| である xi′x_i' に置き換えると、mm は ∣xi∣−∣xi′∣≥1|x_i| - |x_i'| \ge 1 だけ減ります。どちらの候補でも mm は真に減り、mm は非負整数値なので尺度です。定理 5.2 により、反例 xs0xs_0 からの貪欲な縮約は高々 m(xs0)m(xs_0) 回の移動で止まります。

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

演習 9.4標準

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

  • f~1\tilde f_1: 中央値を返す。
  • f~2\tilde f_2: 最小値と最大値の平均を返す。
  • f~3\tilde f_3: 整数のリストに対して、和を要素数で割った商(切り捨て)を返す。
  • f~4\tilde f_4: 先頭の要素を返す。
解答

f~4\tilde f_4 は (a) で検出されます。(1,2)(1, 2) と、並べ替えた (2,1)(2, 1) で、結果が 11 と 22 です。

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

f~1\tilde f_1 と f~2\tilde f_2 は、3 つとも満たすので検出されません。中央値も、最小値と最大値の平均も、並べ替えで変わらず、全要素を 2 倍すれば 2 倍に、11 を足せば 11 増えます。定理 6.2 の言葉では、f~1,f~2∈U(R)\tilde f_1, \tilde f_2 \in U(\mathcal{R}) です。

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

  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 — 性質ベーステストの原論文。生成器と大きさのパラメータ。
  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 — 差分デバッグ 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/ — 生成器(strategies)、設定、状態をもつ系のテスト。

このテーマの 100 本ノック(50 問)

執筆: Claude Code(Opus 5.5)、Claude Code(Sonnet 5.5)・監査 2 回(Claude Code)・最終 2026-10-12

この記事の誤りを報告する ・運営: 夢現技研合同会社 ・料金 ・利用条件 ・特定商取引法に基づく表記

© 2026 夢現技研合同会社 ・コード例は MIT ライセンスです。