Property-Based テストライブラリの暗い現状

 (stevana.github.io)
1 ポイント 投稿者 GN⁺ 2024-07-06 | 1件のコメント | WhatsAppで共有
  • Property-based testingはQuickCheck以降、複数の言語に広がったが、2024年7月時点でも多くのライブラリは、2009年の時点ですでに整理されていた状態ベーステストと並列テストを十分に提供できていない
  • 中核となるギャップは、状態マシンモデルで逐次的な状態変化を検証し、同じモデルを**線形化可能性(linearisability)**検査に再利用して並列実行のrace conditionを見つける機能にある
  • 調査対象の多くでは、状態ベーステストが存在しないか実験的段階にあり、並列テストはさらに少なく、FsCheck、Gopter、RapidCheck、SwiftCheck、jsverifyなどでは関連issueが何年も残っている
  • 約400行のHaskell実装は、状態ベース・並列のproperty-based testingを再現し、従来の状態マシン仕様の代わりに、プログラマになじみのあるfakeベースの参照実装をモデルとして使う
  • 契約テスト済みのfakeは、単一コンポーネントの検証を超えて、実際の依存先の代わりに注入する高速で決定的な統合テストにも再利用できる

QuickCheck以後に生じた機能格差

  • Property-based testingは、「テストを書くのではなく生成せよ」という合言葉のもと、さまざまなプログラミング言語コミュニティへ広がっていった
  • 元祖のHaskellライブラリであるQuickCheckのWikipediaページには、他言語による再実装が57個並んでいる
  • 最初のQuickCheck論文であるQuickCheck: A Lightweight Tool for Random Testing of Haskell ProgramsはICFP 2000で発表され、最初の実装の完全なソースは論文付録の約300行のコードだった
  • 初期のQuickCheckは純粋関数しかテストできなかったが、2002年のTesting monadic code with QuickCheckが、mutable state、file I/O、networkingのような副作用のあるコードを扱う基盤を築いた

状態ベース・並列テストの登場

  • Quviq ABは2006年にJohn HughesとThomas Artsが設立し、EricssonのErlangプロジェクトのテストが初期のユースケースだった
  • Erlangは純粋関数型言語ではなく、並行性も一般的だったため、既存のmonadic QuickCheckだけでは十分に使いやすいものではなかった
  • Quviqのclosed sourceなErlang QuickCheckには、その後の多くのオープンソース実装で欠けていた2つの機能が含まれていた
    • 状態マシンモデルを使う逐次的な状態ベースproperty-based testing
    • 同じ逐次状態マシンモデルを再利用してrace conditionを検出する並列テスト
  • 状態ベーステストはQuickCheck testing for fun and profit (2007)で現在の形として登場した
  • 並列テストはFinding Race Conditions in Erlang with QuickCheck and PULSE (ICFP 2009)で詳しく扱われ、HerlihyとWingによるLinearizability: a correctness condition for concurrent objects (1990)を中核技法としている
  • Quviq QuickCheckのライブラリコードは論文では共有されず、公開されたのはAPIとそのAPIを使うテスト例だけだった

2024年のライブラリ調査結果

  • 現在のstate-of-the-artは、状態マシンモデルに基づくstateful testingと、同じ逐次モデルにlinearisabilityを組み合わせたparallel testingである
  • 調査は2024年7月時点のドキュメント、issue tracker、および一部ソースコードを読んで整理した結果である
  • 多くのライブラリは状態ベーステストを提供していないか、提供していても限定的である
    • QuickCheck(Haskell)は状態ベーステスト追加のissueが2016年から開いたままになっている
    • SwiftCheckも状態ベーステスト追加のissueが2016年から続いている
    • jsverifyは状態ベーステスト追加のissueが2015年から残っている
    • proptest(Rust)では別途proptest-state-machineを参照する必要がある
  • 並列テスト対応はさらにまれである
    • GopterはREADMEに「No parallel commands … yet?」と書かれており、2017年のissueがある
    • FsCheckはparallel support追加のissueが2016年から開いたままになっている
    • RapidCheckはparallel support追加のissueが2015年から開いたままになっている
    • propcheckは2020年からparallel testing追加のissueがある
  • 両機能をサポートするオープンソースの例として、PropEr、Hedgehog、qcheck-stm、quickcheck-state-machine、stateful-checkなどが挙げられている
  • 並列機能があっても制約のある事例がある
    • QuickTheoriesの並列テストは、あり得るend stateの数がコマンド数に応じて急速に増えるため、command listは通常10個以下に制限すべきだとソースコメントに書かれている
    • ScalaCheckのLevelDBとRedisの例は、threadCount = 1の逐次例として示されている
    • fast-checkのrace condition対応は、Quviq QuickCheckの並列テストと異なり、逐次状態マシンモデルの再利用やlinearisabilityの利用には見えない
  • 並列テストが後から追加された明確な例は見当たらず、最初からAPI設計に組み込まれていない場合は大幅な再設計が必要になり得る

機能普及が遅れた理由

  • John Hughesが挙げた理由は3つある
    • 状態ベース・並列テストは純粋関数テストほど有用ではない
    • 状態マシンモデルの作成には通常のテストとは異なる考え方が必要で、教育も必要である
    • open sourceだけでは産業での採用が進みにくく、closed source製品と教育・コンサルティングが採用を後押しした
  • 純粋関数の断片だけをproperty-based testingしても大きな効果は得られるが、産業システムにはdatabase、stateful protocol、concurrent data structureが多く、状態ベース・並列テストもほぼ同じくらい重要である
  • 状態ベース仕様が常に純粋関数仕様より難しいとは限らない
    • key-value storeのモデルは、key-value pairのリストだけでもかなりのところまで表現できる
    • LevelDBの事例では、単純なモデルが数分で17-stepに縮小されたcounterexampleを見つけ、Googleの修正後も再び数分で31-stepのcounterexampleを見つけた
    • 2つ目の問題はbackground compaction processのバグで、compactionは読み取り性能の改善とdisk spaceの回収に重要だが、モデルには明示的に含まれていなかった
  • closed sourceが産業採用を助けた可能性はあるとしても、open sourceの採用には役立たなかったと評価している
  • 論文の結果をQuviq QuickCheckのライセンスなしに再現するには多くのreverse engineeringが必要で、ほぼ不可能だとみている

提案: 小さく公開された実装と容易な仕様

  • 改善の方向性は2つある
    • 元のQuickCheckの約300行実装のように、状態ベース・並列property-based testingの短いオープンソース実装を提供する
    • 状態マシンの代わりに、プログラマがすでになじみのあるmockやtest doubleの概念を再利用して、仕様作成の負担を減らす
  • この仮説を検証するために、2つのことを示している
    • 状態ベース・並列property-based testingを約400行のコードで実装した
    • state machineの代わりに、in-memory reference implementation、つまりfakeをモデルとして使った

純粋な property-based testing の要約

  • 純粋関数のテストでは、入力を生成し、関数の出力が入力とどのような関係を満たすかを確認する
  • たとえば reverse は、任意のリスト xs に対して reverse (reverse xs) == xs という property でテストできる
  • QuickCheck はデフォルトで 100 個のテストを生成し、失敗すると入力を shrink して最小の counterexample を提示する
  • reverse xs == xs のような誤った property は、[0,1] のような最小反例に縮小される
  • よく登場する property パターンには、inverse、idempotency、associativity、abstract data type の公理、metamorphic property などがある
    • inverse: deserialise (serialise i) == i
    • idempotency: sort (sort xs) == sort xs
    • associativity: (i + j) + k == i + (j + k)

状態ベースの property-based testing

  • 状態を持つコンポーネントは、同じ入力が常に同じ出力を生むとは限らない
    • counter の 1 回目の incr の結果と 2 回目の incr の結果は、以前の状態に応じて変わる
    • database や file system も、それまでの入力履歴が次の出力に影響する
  • 純粋関数のテストが単一の入力を扱うなら、状態ベースのテストでは 入力シーケンス を生成し、システムが時間とともにどう変化するかを確認する
  • モデルは m -> i -> (m, o) 形式の fake として表現される
    • 前のモデル状態 m と入力 i から、次のモデルと出力 o を計算する
    • 実際のシステムの出力と fake の出力を各ステップで比較する
    • 不一致があれば入力シーケンスを shrink して小さな counterexample を探す

  • Counter の例

    • グローバル mutable variable を使う Haskell の counter をテスト対象とする
    • incr は counter を増やし、get は現在の値を読み取る
    • モデルは Counter Int 1 つで十分で、StateModel インスタンスは初期状態 Counter 0、Incr、Get、Incr_ ()、Get_ Int、runFake、runReal、command generator を定義する
    • incr42Bug のように counter の値が 42 のとき増加しないバグを入れると、QuickCheck は 66 個のテスト後に失敗を見つけ、29 回 shrink して 43 回 increment した後に Get する最小反例を提示する
    • テストの間で実際のグローバル counter を reset しないと、モデルは常に 0 から始まる一方、実際の counter は前のテスト状態を保持するため mismatch が発生する

  • 状態ベースライブラリのインターフェース

    • StateModel インターフェースはテスト対象システムを black box と見なし、command を入力、response を出力とする
    • 中核となる構成要素は Command state、Response state、initialState、runFake、runReal、generateCommand である
    • optional な構成は次のとおり
      • Reference: file handle のように、前の response が作ったリソースを後続の command で参照するときに使う
      • PreconditionFailure: 開かれていない file handle から read できない、といった precondition の失敗を表現する
      • CommandMonad: デフォルトは IO だが、別の monad も使える
      • monitoring, commandName: coverage と統計に使う
    • command 生成時には実際の file handle のような値は作れないため、Var Int 形式の symbolic reference を生成し、実行中に実際の reference に置き換える
    • shrink 後は、precondition を破る command や scope 外の symbolic reference を使う command を取り除く

  • Circular buffer の例

    • C で書かれた circular queue を Haskell FFI でテストし、モデルは単純なリストベースの queue として記述する
    • C 実装は error checking をしていないため、empty queue で get すると初期化されていない memory を返す可能性がある
    • 実際の実装は circular index によって効率的だが、明白に correct とは言えず、fake は効率が劣ってもテスト用なので問題ない
    • new が queue reference を返すため、モデルは Map (Var Queue) FQueue で複数の queue を管理する
    • 最初は full queue への put に対する precondition が抜けており、サイズ 1 の queue に 0、1 を入れて get すると、モデルは FIFO なので 0 を期待するが、C コードは 1 を返す
    • これは実装バグではなくモデルの precondition 漏れなので、QueueIsFull precondition を追加して修正する
    • Size command が generator から漏れていたことは coverage 出力で判明し、これを追加すると queue size 計算バグが見つかった
    • サイズ 1 の queue に item を 1 つ入れて Size すると期待値は 1 だが実際の値は 0 であり、new で内部 buffer サイズを n + 1 にする修正が提示される
    • その後、abs(q->inp - q->outp) % q->size はサイズ 1 では通るがサイズ 2 で再び失敗し、最終的な修正は (q->inp - q->outp + q->size) % q->size である

  • Die Hard 3 の水差しパズル

    • 3L と 5L の水差しで正確に 4L を作るパズルを、状態ベーステストで解く
    • 実際の実装がなくても、モデルと fake だけを実行し、特定の状態に到達したらテストを失敗させることで shrink された action sequence を得られる
    • 199 個のテストと 11 回の shrink の後に提示された sequence は次の流れである
      • 5L の水差しを満たす
      • 5L から 3L に注ぐ
      • 3L の水差しを空にする
      • 5L から 3L に再び注ぐ
      • 5L の水差しを満たす
      • 5L から 3L に注ぐ
    • trace には中間状態が表示され、big jug が 4L になる過程を確認できる

並列 property-based testing

  • concurrent code のバグは、thread interleaving が実行ごとに異なるため、再現と修正検証が難しい
  • 目標は、ユーザーが追加のテストコードをあまり書かなくても、逐次状態ベーステストのように並列テストをできるようにすること
  • counter の例で、incr が readIORef の後に writeIORef を非原子的に実行すると、2つの thread が互いの increment を上書きして race condition が発生する
  • 並列テストでは、実行中の command の invocation と response の時点を集めて concurrent history を作り、その history がどの逐次 interleaving で説明できるかを検査する
  • どれか1つでも interleaving が逐次モデルと一致すれば、その history は linearise するとみなし、correct と判断する
  • どの逐次 interleaving でも実際の response を説明できなければ、non-linearisable な結果として扱われる

  • 並列 command の生成と shrink

    • 並列プログラムは ParallelCommands と複数の Fork で表現され、各 Fork 内の command は並列に実行される
    • 例の実装では、single、double、triple threaded execution を扱う
    • 並列実行では、Fork [Write "a" "foo", Write "a" "bar"] のように interleaving によって可能なモデル状態が変わりうる
    • 並列モデルは単一の state ではなく、state の集合 を基準に command の生成と shrink を行う
    • parallelSafe は、Fork 内 command のすべての permutation で precondition が維持されるかを確認する
    • たとえば Write "a" と Delete "a" が同じ fork にあると、ある command が別の command の precondition を壊す可能性がある
    • shrink の過程でも、precondition と symbolic reference scope を維持する command だけを残す

  • 並列実行と linearisability 検査

    • 並列実行では、各 command の Invoke と Ok event を history に記録する
    • response に新しい reference が含まれる場合は、atomic counter で環境を拡張して thread 間の reference 番号衝突を避ける
    • history から可能なすべての interleaving を Rose tree として列挙する
    • linearisable は、この tree のいずれかの path が逐次 runFake モデルと response を一致させるかを確認する
    • 並列テストは結局逐次モデルを再利用するため、ユーザーは逐次モデルを書いた後、少ない追加コードで並列テストを得られる

  • Parallel counter の例

    • counter の並列テストを有効にするために追加したコードは、ParallelModel Counter インスタンスと property だけ
    • 非原子的な incrRaceCondition を使うと、race condition を見つけられる
    • より小さい test case にも race があっても、別の interleaving のせいで失敗が再現されなければ、QuickCheck はその小さい test case は通るとみなして shrink を止めることがある
    • 正しい解決策は deterministic thread scheduler であり、並列テストの論文ではこれを使っている
    • 例の実装では、より単純な workaround として shared memory の read/write の前後に短い sleep を入れ、同じ interleaving が起きる可能性を高めている
    • sleep は race を見つけるためではなく、見つけた race の counterexample を小さくするために必要になる
    • sleep を追加すると、最小反例は ParallelCommands [Fork [Incr,Incr],Fork [Get]] に縮小される

  • Process registry の例

    • Erlang の process registry のように、thread を spawn し、名前で ThreadId を register・lookup・unregister・kill するシステムを例として使う
    • 逐次モデルは、生成された thread id、登録済みの name-thread pair、kill 済みの thread id を追跡する
    • Register と Unregister は失敗しうるため、response には Either ErrorCall () を使う
    • 実際の実装の error location 情報は、fake と合わせるために abstractError で取り除く
    • monitoring は RegisterFailed、RegisterSucceeded、UnregisterFailed、UnregisterSucceeded の coverage を示す
    • 意図的に register が既存の registry を上書きするバグを入れると、すでに登録した "e" を unregister できない逐次反例が現れる
    • 並列テストではより長い反例が現れ、SleepyIORef を使うと Fork [Register "b" (Var 0), Register "c" (Var 0)] という形に shrink される
    • 問題は、readRegistry で確認した後 atomicModifyIORef を呼ぶまでの間に別の thread が割り込める race である
    • register、unregister、kill に global lock を適用した後、並列テストは通る

Fakeベースのモデルと統合テスト

  • 従来の state machine specification with post-conditions の代わりに、インメモリの fake を reference implementation として使う
  • Edsko de Vries の 2019年の記事 は、fake を post-condition ベースの状態機械仕様の上に実装する方法を提案した最初の記事として紹介されている
  • fake は mock に似ており、formal specification に慣れていないプログラマにとってより容易なアプローチとして提示される
  • fake には、統合テストで依存コンポーネントの代わりに使えるという利点もある
    • 実際の dependency を起動したり有効化したりする必要がない
    • より高速で deterministic な integration test を構成できる
  • fake が間違っている可能性があるという問題は contract test で扱う
  • 状態ベース・並列 property-based test が fake と実装の一致を検証するため、fake は契約テスト済みの依存関係として機能する

  • Queue fakeによるテストとデプロイの分離

    • queue インターフェース IQueue は iNew, iPut, iGet, iSize を持つ
    • 実際の実装は C queue wrapper をそのまま接続する
    • fake 実装はモデル状態を IORef に保存し、fNew, fPut, fGet, fSize を通じて更新する
    • コンポーネントは IQueue q インターフェースに対して記述される
    • テストでは fake インスタンスを使い、デプロイでは real インスタンスを使う
    • 状態ベースの property-based test により、fake が real に faithful であるという前提を置く

  • File system fake

    • file system インターフェース IFileSystem h は iMkDir, iOpen, iWrite, iClose, iRead を持つ
    • 実際の実装は /tmp/qc-test 配下の実際の file system を使う
    • fake は directory set、file content map、open handle map、next handle を持つインメモリの FakeFS として実装される
    • fOpen, fWrite, fClose, fRead は、使用中の file、存在しない directory、閉じられた handle のような precondition failure をモデル化する
    • fake file system が実際の file system と faithful であるとテストされれば、file system に依存するコンポーネントは fake で integration test し、デプロイ時に real file system に置き換えられる
    • real に置き換えたときにバグが発生したら、fake と real の不一致が状態ベースの property-based test をどう通過したのかを調査しなければならない

  • より大きなコンポーネントシステム

    • A が B に依存し、B が C に依存するシステムも同じ方法で拡張できる
    • 各コンポーネントにインターフェースを置く
      • iC :: IO IC
      • iB :: IC -> IO IB
      • iA :: IB -> IO IA
    • テスト戦略は次のとおり
      • C を状態ベース・並列 property-based test で検証して、contract-tested な fake C を得る
      • B の integration test では fake C を使う
      • A のテストでは、fake C を使う fake B を使う
    • この方法は、より多くのコンポーネントやサービスにも同じパターンで拡張できる

結論

  • 状態ベース・並列 property-based testing はおよそ400行のコードで実装でき、これは shrinking のなかった初期の QuickCheck の約300行の実装と比較可能な規模である
  • fake をモデルとして使うと、状態ベース・並列テストの仕様記述がより馴染みやすい形になり、より大きなシステムを compositional にテストする際にも再利用できる
  • 各言語コミュニティが実験を続ければ、property-based testing ライブラリの現状を改善する余地がある

関連記事

1件のコメント

 
GN⁺ 2024-07-06
Hacker News の意見

  • カバレッジガイド付きファジングが登場し、Go でも十分サポートされているのに、プロパティベーステストライブラリを使わないと何を見逃すのか気になる
    https://www.tedinski.com/2018/12/11/fuzzing-and-property-tes...
    下のファズテストと、それに対応する不変条件の検査を見ると、実質的にはプロパティテストとほとんど同じではないかと思う
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...

    • プロパティベーステストとファジングの区別は、だいたい雰囲気で大まかにまとめたものに近い
      実際の違いはあるが境界はかなり曖昧で、何がファジングで何がプロパティベーステストなのかを正確に線引きすることは、それほど重要ではない
      高速に回るテストと詳細なアサーションはプロパティベーステスト、長時間回してクラッシュだけを探すものはファジング、その中間は曖昧
      https://hypothesis.works/articles/what-is-property-based-tes...
    • カバレッジガイド付きファジングとプロパティベーステストは十分に組み合わせられる
      Google にいたとき、この2つを組み合わせた社内ツールが本当に良かった。いつものようにプロパティベーステストを書くと、実行時にテストフレームワークがカバレッジを取得するよう特別にコンパイルし、ランダム入力を調整してカバレッジを増やす。もちろん複数マシンのクラスタ上で完全に自動実行する
      伝統的なプロパティベーステストは通常ライブラリだけで実装されるため、ランダム入力生成を導くためのカバレッジ情報が必ずあるわけではない
    • プロパティをアサートしているのだから、「レベルが1より大きいすべてのノードは子を2つ持つ」のような定義上、プロパティベーステストに該当すると考える
      ただしライブラリによっては便利な機能をかなり得られる。あるとよいものの1つが shrinking（縮小）で、ここの「Shrinking」セクションを参照すればよい: https://tech.fpcomplete.com/blog/quickcheck-hedgehog-validit...
      ジェネレータを組み合わせるコンビネータも優れており、ライブラリによっては例外的な挙動を引き起こす既知の「悪い」値の集合を持っていることもある
    • Go のファズテストがリンク先の記事の内容とどう違うのかはよく分からないが、その記事では、まともなファザーは数日から数週間走らせるべきで、プロパティベーステストはファジングよりほぼ常に選ぶべきだと述べていた
      一歩引いて、テストについてもう少しメタな問いを投げかけたい。テストの成功はコードの成功を意味し、その逆も成り立つのか。Go の契約の中に、同じ入力を同じコードに入れれば同じ出力が出る、と明記している箇所はあるのか？
    • API の観点で主に得られるのは、望むランダムなデータ構造を生成するコンビネータライブラリである
      ランダムオブジェクトの集合を表す Arbitrary 型を扱うと、テスト入力を生成する再利用可能な関数を簡単に書ける。そのようなライブラリは Go のファジングフレームワークともかなり簡単に併用できそうだ
      それでも map、filter、chain、oneOf のような一般的なコンビネータは少し扱いにくいかもしれないと思っており、JavaScript 向けの新しいプロパティテストライブラリを書いている。より使いやすくするのが目標だが、まだ実験的で公開前である

  • clojure.spec.alpha は、test.check と併用するかどうかにかかわらず素晴らしい体験だったが、Python の hypothesis を使ってみると本当にひどかった
    Hypothesis は単純だが「大きな」データセットを設計上扱えないように見えた。ここでいう「大きい」も、実際にはそれほど大きくない。[0] あまりにつらかったので、職場の Python テストスイートから Hypothesis と生成ベースのテストを完全に取り除いた
    [0] https://github.com/HypothesisWorks/hypothesis/issues/3493

    • この場合、Hypothesis が大きなデータセットを扱えないというより、縮小されたケースのかなりの数を拒否していたように聞こえる
      Hypothesis は、バグが 0 でも存在するかを見ようとして、生成された整数を 0 に縮小しようとし、テストは 0 が含まれているという理由で失敗ではなく拒否していた。小さなケースでは非効率にとどまったが、大きなケースでは Hypothesis が諦めるほどになった
      そのスレッドでは、誰かが 0 を生成できない別のインスタンス生成戦略を使うよう提案していた。Hypothesis の shrinker が最も好む値を生成してから拒否するのではなく、最初から作らない方式だ。それを試してみたのか気になる
      clojure.spec.alpha がこれをどう違った形で扱うのかも気になる
      https://news.ycombinator.com/item?id=40876437 の mjaniczek のコメントでは、この例を Hypothesis のアプローチの欠点として挙げている
      「生成器が、失敗しうるバイト列パーサーになるので多少の非効率が生じ、ユーザーが内部 shrinker では完全には縮小できない奇妙な生成器を作れてしまう。それでも 3 つのアプローチの中では開発者体験が最も良い…」という趣旨だ
      もちろん、本人は自分のテストを「奇妙な」書き方で書いたとは同意しないだろう
    • Clojure の spec は周辺を組み立てるのが本当に簡単で良かったが、Elixir に移ってからは、そういうテストを書くには古い Erlang ライブラリである propEr まで降りる必要があった。かなり残念だ
    • GitHub issue に載っている例は、filter を自ら問題を引き起こす形で使っている
      ランダムに生成してから何らかの属性に合うものを絞り込むと、生成過程で実質的に宝くじを削っているようなものになる

  • 記事が投げかけている「発表された研究は、オープンソースのツール、あるいは少なくとも一般の人々や他の研究者に無料で提供されるツールで再現可能であることを求める要件がなぜないのか？」という問いへの簡単な答えは、その要件の即時の結果として、その条件を満たせない論文は発表されなくなるということだ
    たとえば、著者や他の人々にとって有用だったと思われる Quviq QuickCheck 論文 のようなものも発表されなかっただろうし、コミュニティはその情報という贈り物を失っていただろう

    • 一部の出版社は再現可能性を求め、一部は求めない、という形なら良いと思う
      すべての要件には排除効果があり、要件を満たさなくても有用でありうる論文という境界事例は常に存在する
    • これは明確に白黒がつく問いではなく、政治的な問いとまで呼べるかもしれないが、だからといってこの擁護論はあまり有効ではない
      この論理を有効だと見なすなら、それを盾にしてどこまでも行けてしまう。再現可能性を要件から外せば、説明したくないものは何も説明しなくてよくなる。標本に関するデータも、統計的有意性検定も提供する必要がない。何らかの結果を達成したと主張する曖昧な要旨だけで十分になる
      さらには、フェルマーが『算術』の私蔵本の余白に残した有名なメモさえ、完全に有効な研究論文になる。有名な数学者がある定理について簡潔で優雅な証明を持っていると考えていた、という貴重な情報を失いたくはないだろうからだ。もちろん実際には存在しなかった可能性が高いが
      この政治的な問いに対する私の考えは、現在の基準は緩すぎるというものだ。誰も何かを発表するよう強制されてはいない。世の中には独占的価値などの理由でどこにも発表されない研究が多くあり、そうした研究が消えることはないだろう
      しかし学界で働き、まして研究費まで受け取り、世界の科学知識を前進させることが目標だと言うなら、実際にその目標に従うよう求めるのは公正だ。ただ学界でのキャリアの梯子を上るためだけに、その目標に従っているふりをしてはいけない
    • ソースコードを査読者にだけ公開する方式も可能なのではないかと思う
      コードを実行するのに必要なものも一緒に提供すればよい。すでにそうしているのかもしれない
    • 再現可能性は科学的方法の礎だからだ
    • 論文は、著者たちが「重要度指数」を高めたいがために発表されるものであり、それは報酬や学界でのキャリアの可能性と非常に直接的につながっている
      その目的のためであれば、要件がさらに増えたところで発表論文数が減る可能性は低い
      発表論文におけるより深刻な問題は、できるだけ多く、速く発表しようとして、意図的にミスを見過ごすことが多い点だ。論文の検証が容易になればこの状況が改善される可能性はあるが、大きく期待はしない。人々は近道を見つけるのが非常に得意だ

  • Rust の proptest でステートフルなプロパティテストをかなり頻繁に書いており、たいていは自分でコーディングするが、かなり簡単です
    6 件のバグを見つけた非自明な例は https://github.com/sunshowers-code/buf-list/blob/main/src/cu... にあります
    並列テストはときどき役に立つかもしれませんが、単に多数のテストを並列に走らせるほうが簡単な場合が多いです

    • Rust で手動のプロパティテストをよく書きますが、だいたいこのような形です
      最上位では本当のランダム性を使い、その下にネストしたループをいくつか置いて、低い複雑度のケースから高い複雑度のケースへ上げていきます。次に、決定的な疑似乱数生成器に与えるシードを作り、出力しておきます。テストが失敗したら、エラーになったシードをコピー＆ペーストして失敗ケースを再現できます
      こうした手動プロパティテストは、どんなフレームワークやライブラリよりも速く、柔軟で、全体として手間が少ないと感じました
      ただし、本当に堅牢な並行性テストには AWS Shuttle ライブラリ（https://github.com/awslabs/shuttle）を強く勧めます。信じられないほど複雑な競合状態を見つけられます。短いチュートリアルも書きました: https://grantslatton.com/shuttle
      AWS では、AWS S3 を動かすために書いたカスタムファイルシステムの検証にこのライブラリを使っていました

  • リンク先の “Testing Telecoms Software with Quviq QuickCheck” 論文をざっと眺めましたが、「なぜこのステートフルな作業を自分で作るほうがよくないのか？」という問いへの答えはすぐには見当たりませんでした
    原文はキー・バリューストアのキー・バリューのペアモデルでこの部分を示していますが、なぜ単に状態機械を書いてはいけないのか、なぜフレームワークが必要なのか分かりません。先週、職場でファイルシステムの相互作用テストのために文字どおりそうしましたし、結局 type Instruction = | Read of stuff | Write of stuff | Seek of stuff | … 程度に落ち着きました
    そうするとプロパティは「この命令リストが与えられたとき、…」になります。StateModel 形式も基本的に同じことを求めています。StateModel が十分に役立っているとは見えず、理解すべきフレームワークコードをはるかに多く追加する代わりに、実際の経験上ごく少量のテストコードをなくすだけの利益しかないように思えます

    • その判断が正しいテストもありますが、失敗ケースを縮小する部分が難しいことが多いです
      「有効な」状態遷移シーケンスだけを生成したいなら、特定の状態でどのテストステップが有効かを決めるモデル状態が通常必要です。また、縮小中にテストステップを削除した結果、もともと各ステップを生成するときに守っていた事前条件を壊して偽の失敗が出ないようにする必要もあります
      どんな状態でもどんな操作も有効で、完全にランダムな任意の操作シーケンスだけが欲しいなら、ステートフルな proptest フレームワークは過剰かもしれません。しかし、モデル状態を維持し、複数の操作の事前条件を指定する必要があるなら、専用フレームワークは多くの作業を肩代わりしてくれます
      昨年このテーマでブログ記事を書いたので、より深い例に興味があれば参考になるかもしれません: https://readyset.io/blog/stateful-property-testing-in-rust
      他の人も言っているように、並列状態機械テストも専用フレームワークで得られる素晴らしい利点ですが、それが唯一の利点ではありません
    • ステートフルな部分はモデルベーステストのほうがうまく扱えると思います
      テストスタイルは混ぜて使っても構いません。自分のコードなのですから
    • 並列 QuickCheck は、マルチスレッドプログラムで起こり得るすべてのインターリービングが、最終的にコマンドを逐次呼び出した場合にも到達可能な状態を作るかどうかを確認するものだと理解しています
      それが利点です

  • 筆者はプロパティベーステストの状態機械と並列の側面に注目しているが、より大きな効果があり得る別の側面もある
    1つはカバレッジ誘導型プロパティベーステストで、Dan Luuの記事を読むとよい: https://danluu.com/testing/
    もう1つは私に偏りがある分野だが、値を生成するときに作ったすべての不変条件を維持しながら、縮小を自動化することだ
    要約すると、値に作用するQuickCheck式の派生縮小関数（shrink : a -> [a]）には制約条件と問題があり、人々は問題に対処するよりも縮小を切ってしまうようになる
    ローズツリーによる「統合縮小」（例: Hedgehog）は生成器の制約条件には従うが、モナドのbind、つまり生成器の結果を使って別の生成器へ分岐する場合に問題がある
    魔法のように「ただ動く」ように見える唯一のアプローチは、Hypothesisの内部縮小だ。値そのものではなく、ランダムな選択のリストを小さくする間接層を使う。欠点は、生成器が失敗し得るバイト列パーサーになり、多少の非効率が生じることと、内部縮小器が完全には縮小できない奇妙な生成器をユーザーが作れてしまうことだ。それでも3つのアプローチの中では開発者体験が最もよく、人々がテストをすること自体が小さな奇跡だと考えると、テストライブラリ作者として最も構築する価値があるアプローチのように感じる

    • ローズツリーによる「統合縮小」（例: Hedgehog）が生成器の制約条件には従うがモナドのbindに問題があるという点は、私の素人知識の範囲ではモナドbind/生成器の根本的限界だと思う
      代わりに、最適な縮小のためにはapplicative生成器を好むべきだ: https://github.com/hedgehogqa/haskell-hedgehog/issues/473#is...
      言い換えると、applicative生成器は「生成器の結果を使って別の生成器へ分岐」せず、applicativeの「並列」な性質によって縮小が最適化される。ここでの並列は記事におけるスレッドの意味ではなく、モナド的な意味だ。applicativeは「並列」なので、生成器を独立に小さくできる。一方、モナド生成器は「直列」なので、1つを小さくすると後続の生成器の動作が必ず変わる
      公開されている発表ならリンクを見たい
    • 個人的には、Hypothesisは「ただ動く」とは程遠かった
      実際にプロダクション対応だとは思っておらず、それも設計上そうなっているように見える。[0]
      clojure.spec.alphaをtest.checkと併用したり単独で使ったりかなり経験していたので、違いがあるにしても一般的な考え方に完全に不慣れだったわけではない
      [0] https://github.com/HypothesisWorks/hypothesis/issues/3493
    • 私が好むフレームワークはfalsifyで、「内部統合縮小」を提供している
      Hypothesisに似ているが、線形シーケンスではなく生成器ツリーを使う。selective functorに基づいており、これはバリデータのようなものにも役立つ良いインターフェースだ
      https://hackage.haskell.org/package/falsifyによれば、このライブラリは内部統合縮小をサポートするプロパティベーステストを提供している。Hedgehogの意味での統合、つまり別々の縮小器と生成器を書く必要がないという意味であり、Hypothesisの意味での内部、つまりモナドbind全般でもうまく動作するという意味だ

  • プロパティベーステストを使ってみようとしたが、いつも二つの椅子の間に挟まっている感じがした
    あるプロパティを厳密にテストできるほどよく理解しているなら、たいてい型システムに押し込んで構成上真になるようにできる。単に簡単なスモークテストがほしいだけなら、任意の入力を1つ使うほうが簡単だ

    • どんな種類のプロパティを念頭に置いているのか気になる
      例えば、遅いが単純な素朴な実装と最適化された実装の2つがあることは多く、任意の入力について両者の出力を比較できる。理解しやすい単純なプロパティだが、一般に型システムへ入れるのは難しい
      同様に、入力が提示される順序は重要でないはずだとか、データを分割できる方法があり、max(Aの最大値, Bの最大値) = maximum(A union B)のような性質がある場合もある。こうしたものを型システムでどうエンコードできるだろうか？
      あるいは「任意のAとBについて、Aで見つけたある最適解は、A union Bで見つけたある最適解より悪くない」のようなものや、f(f(A)) = f(A)のような冪等性もある
      これらはいずれも理解しやすいプロパティだが、ほとんどの型システムで表現するのは簡単ではない
    • 可能ならコンパイル時に制約を強制するほうが明らかによい
      しかし、主流の型検査器では扱えない制約も多い。依存型は大いに役立つだろうが、まだ定理証明器のようなニッチに限られているように見える

  • 一覧から元祖のQuviQ Erlang QuickCheckが抜けているのではないかと思う
    製品全体はプロプライエタリだが、無料版のQuickCheck Miniも提供されている: http://www.quviq.com/downloads/

  • Clojureにも今では状態を持つquickcheckライブラリがある: https://github.com/griffinbank/test.contract
    並列テストは興味深いが、まだ大きな苦痛の源にはなっていない

  • C#/.NET のテストでは CsCheck[0] を使ってきており、かなり満足していた
    Hedgehog や FsCheck よりずっと取り組みやすく、速度もかなり速い
    [0] https://github.com/AnthonyLloyd/CsCheck