性質の試験を作る

例の試験は、誰かが思いついた入力を 1 つずつ確かめる。この検査は、入力の揺れの一覧を決め、その組み合わせを道具に多数作らせ、どの入力でも成り立つ性質を確かめる。見つける力は乱数でなく、一覧で決まる。bb-writ 自身の作業の記録の欄の解析で、雛形と一般的な揺れだけから作った生成器は、審査で 3・4 周目に見つかった不具合を 4 件のうち 1 件も見つけなかった。手入力の揺れを 7 通り並べただけの一覧は、空の欄が push の関門を通る入力を見つけた。ただし、手元の実際の記録 202 件にその書き方は 1 度も無く、揺れを読み分ける解析器を足して塞ぐと、審査の周ごとに新しい穴が出た。目的は「通った」と言うことでなく、実物の不具合を見つけ、一覧の外を正直に示すこと。

1. 対象を選ぶ

外から来た入力を読む・変える・切り詰める所を、コードと履歴から選ぶ。解析（記録・設定・コマンドの出力・URL・パス）、整形と往復（書いて読み戻す）、上限と切り詰め、パスや種類の判定。git log で同じ関数の入力の形の修正が続いた所、審査の指摘に「全角」「BOM」「非 UTF-8」「symlink」「改行」が出た所が候補。

順序・交互実行・途中の kill・再開・記録をまたぐ状態は、この検査でなく create-formal-verification-skill で全部の順序をたどる（乱数で選んだ順序は、その一部しか見ない）。

2. 約束を文にする

約束を 1 文ずつ、コードの言葉で書く。それぞれ、破れたときの被害も 1 文で書き、危ない側（通してはいけないものを通す）か安全な側（正しいものを拒む）かを分ける。答えの出し方は、次の順に強い。

• 組み立てから答えが分かる: 答えを決めてから入力を組み立てる（空にした欄を覚えておき、関門がその欄だけを挙げるか）。最も強い。
• 往復: 書いて読み戻すと元に戻る。
• 不変条件: 上限を超えない、出力が入力の接尾辞になる、件数が保たれる。
• 別の作りとの一致: 遅いが明らかに正しい作りと結果が同じ。

対象のコードと同じ手順を試験に写して答えを出さない（同じ誤りを同じに写し、何も確かめない）。

3. 揺れの一覧を出所から作る

一覧は思いつきで作らず、次の出所を全部たどって作る。行ごとに、出所・揺れ・期待（受ける・拒む・中身に数える）を書く。

• 仕様と雛形: 名前の付いた要素ごとに、雛形どおり、省ける部分を省いた形、別の文言を入れた形、2 回目に現れる形。
• 手入力の揺れ: 全角と半角（記号・括弧・空白・コロン）、箇条書きの記号の種類、名前の前後の空白、大文字と小文字、タブ、CRLF、先頭の BOM。
• 形式の記号: その形式（Markdown・YAML・シェル・URL など）の記号ごとに、記号だけの行と、記号で始まるが記号でない行（「#」だけの行と「#12 の件」）、字下げ・入れ子・表・引用。
• 文字コード: 多バイト文字・絵文字・NUL・JSON で伸びる文字（"・制御文字）・UTF-8 でないバイト。
• 大きさの境界: 空、1 つ、読み込みの窓・バッファ・上限のちょうど前後、境をまたぐ多バイト文字。
• OS とファイル: symlink（一時ディレクトリが symlink の下にある macOS を含む）、壊れた symlink、大文字と小文字を区別しない置き場、通常のファイルでないもの。
• 過去の修正: git log の修正の commit と審査の指摘から、直した入力の形を全部。

期待が仕様から決まらない行は、推測で決めない。仕様の問いとして利用者に返すか、戻せる選択なら既定を決めて理由を書く。拒むと決めた揺れが、別の欄や前の要素の中身に数えられて危ない側に倒れないかも、行ごとに見る（全角の「：」の欄の行を欄と見ないと、その行が前の空の欄を埋めた）。倒れる行は、6 のとおり実際に起きるかを数えてから、直すか守らない範囲に書くかを決める。

4. 生成器を書く

既定は、対象の言語の定番の道具を、試験だけの依存として使う（Python は Hypothesis、JavaScript・TypeScript は fast-check、Rust は proptest、Go は rapid、Haskell は QuickCheck）。縮小（反例を最小の形まで縮める）が使えるため。依存を足すことが依頼の範囲を超えるなら、利用者に聞く。対象の規則が依存の追加を禁じているか、聞いて足せないと決まったら、seed を固定した標準の乱数で回し、縮小が無いことを報告に書く（規則が禁じているときは聞かない。試験だけの依存も禁じているか読み取れなければ聞く）。

• 道具の版は、対象の CI が回す言語の版ごとに入るものを、配布元の情報（PyPI の requires_python など）で確かめてから固定する（Hypothesis は版によって古い Python を受けない）。
• 道具が無い環境では、飛ばした理由が出力に残る形で飛ばす（件数 0 のまま黙って通さない）。CI は入れて回す。
• CI は毎回同じ入力で回す（Hypothesis の derandomize、固定の seed）。広く回すときは、環境変数などで例の数を増やし、乱数を変える。例の保存場所をリポジトリに残さない。
• 一覧の行が実際に生成されることを、一度数えて確かめる。道具の既定の分布は小さい値に寄り、窓や上限の境に届かないことがある（短い並びと境をまたぐ長い並びを、別々の範囲から引く）。
• 普段の実行は数秒以内を目安にする。

5. 落ちるのを見る

性質ごとに、コードを壊した版を作り、試験が落ちることを示す。壊し方は、過去の修正を戻した版（変えた hunk を 1 つずつ戻す）と、一覧の行ごとの扱いを 1 つずつ外した版。道具がある実行と無い実行の両方で当てる。一度も落ちていない性質は、確かめたと書かない。

壊した版が通ったら、理由を確かめる。生成器がその入力に届いていない（見出しが必ず先頭にあり、BOM が欄の行に付かなかった）なら、生成器を直す。届く入力のどれでも結果が変わらない（既定の上限が窓より小さく、窓の先頭が必ず削られた）なら、上限など呼び出し側が決める値も生成の対象に入れるか、変わらない理由を試験の文に書く。どの入力でも変わらないなら、そのコードは要らないので削る。結果は変わるのに性質がその違いを見ていないなら、性質を強める（答えを組み立てから出す形に近づける）。

6. 反例を不具合にする

縮小した反例は疑いで、まだ不具合ではない。利用者が通る経路（CLI・関門・API）で再現する。直す前に、その入力が実際に起きるかを実物の入力（手元の記録・ログ・利用者のファイル・過去の Issue）で数える。生成した揺れは実際に起きない形を多く含む。起きない形のために解析を足すと、足した所に次の穴が出て審査の周が止まらない。起きないなら、依頼が「直して」でも解析を足さず、数えた結果とともに守らない範囲として試験とコードの文に書き、返答で利用者に返す。その形は生成器から外し、試験の冒頭の「省いたもの」に書く（性質を弱めるのでなく、範囲を文に書く）。その形を、直した後の振る舞いを期待する固定の例にはしない。守らないと決めた今の振る舞いを文書どおりに固定する例は、残してよい。仕様の問い（期待が決まっていなかった）か、不具合か、生成器か答えの誤りかを分ける。性質を弱めて反例を消さない。実際に起きる形で再現した反例と境界の例は、道具が無い環境でも回る固定の例の試験として残す（道具が無いと性質の試験は飛び、手元の実行では退行が通る）。実際に起きる入力の不具合のコードを直すかは、依頼に従う（調べるだけの依頼では直さない）。

7. 範囲を分ける

この検査は、一覧に無い揺れを見つけない。順序と止め方は create-formal-verification-skill、届ける前の審査は interrogate で別に通す。

8. 残す

対象のリポジトリの既存の試験に、1 コマンドで回る形で置く。依頼が調べるだけ（変更しない）なら、リポジトリには置かず、写しで動かして証拠の置き場に残し、置き方を返答で提案する。試験の冒頭に、約束、揺れの一覧（出所ごと）、省いた出所とその理由、道具と設定（固定の入力・広く回す方法）、確認した commit を書く。依存は試験だけの置き場（requirements の試験用のファイルなど）に、版を固定して書く。

返す形

確かめた約束（危ない側か安全な側か）、揺れの一覧と省いた出所、道具とその理由（依存を足したか）、落ちるのを見た壊し方（通った壊し方とその理由）、見つけた不具合（縮小した反例と、実物での再現の結果）、一覧の外に残る範囲、再実行の 1 コマンド。「検証済み」と 1 語で書かない。