はじめに
こんにちは、株式会社Techouseでバックエンドエンジニアをしている satoh(@shiro-tec) です。
本記事では、RubyKaigi 2026 の Day2 で発表された Masato Ohba(@ohbarye) さんによるセッション「From Formal Specification to Property Based Test」について紹介させていただきます。
このセッションは、@ohbarye さんが RubyKaigi 2024 で発表された「Unlocking Potential of Property Based Testing with Ractor」の続編にあたる内容です。形式仕様（Formal Specification）から、プロパティベーステスト（Property Based Testing）を自動生成するというテーマで、Ruby向けに開発された spec-to-pbt というツールが紹介されました。
From Formal Specification to Property Based Test
モチベーション
ソフトウェア開発では、仕様を書き、実装を行い、テストを書くという流れが一般的です。しかし、ここには2つの問いが残ります。
- 書かれた仕様が正しいか
- 書かれたテストは実装の正しさを十分に検証できているのか
特に AI が実装やテストを生成することが増えるこれからの時代では、これらの問いに対する答えを持っておくことが重要であると指摘されました。
Formal Specification と Property Based Testing
この2つの問いに対して紹介されたのが、Formal Specification と Property Based Testing です。
Formal Specification（形式仕様）は、形式手法の一部であり、数学や論理学をベースとした言語で仕様を記述する手法です。自然言語による仕様と異なり解釈の余地がなく、仕様内の曖昧さや矛盾を機械的に検出できます。
Property Based Testing（PBT）は、テストにおいて「期待する出力」ではなく「満たすべき性質」を記述する手法です。ジェネレータと呼ばれるプログラムが生成するランダムな入力に対して、満たすべき性質が破れないかをテストします。
組み合わせのねらい
PBTを生成する仕組みに非決定性が含まれていると、生成されたテストコードと仕様との結びつきが追えなくなり、品質保証として機能させることが難しくなってしまいます。ここで、形式仕様を入力として、そこから決定的にPBTを生成できれば、生成されたテストコード自体が仕様を反映したものとして一定の信頼性を持つことになります。
そこで @ohbarye さんは、Ruby でこれを実現するツールとして spec-to-pbt を自作されたと紹介されました。
spec-to-pbt の構成
spec-to-pbt は、形式仕様を入力としてPBTのコードを出力するRuby向けのツールです。
具体的な入力:
- 形式仕様: Alloy（
.als）または Quint（.qnt）で記述
具体的な出力:
- pbt gem 用のテストファイル
- ユーザーが編集する設定ファイル
現状はステートフルPBT（状態を持つシステムを対象とするPBT）に特化した設計となっており、ステートレスPBTは未対応であるとのことです。
ツール内部は3層構造のアーキテクチャとして設計されており、Frontend（入力のパース）、Analysis（仕様の解析）、Generation（テストコードの生成）の3つの層に分かれていると紹介されました。
デモ
セッションでは、Stack を題材としたデモが紹介されました。
形式仕様には、Stack が後入れ先出し（LIFO）で動作するべきことが記述されています。一方で、Ruby実装側では誤って先入れ先出し（FIFO）として実装されている、というシナリオです。
spec-to-pbt が形式仕様から自動生成したPBTを実行すると、push(0) push(-1) pop という操作列で反例が検出され、仕様と実装が一致していないことが指摘されました。人手で書かれたテストケースでは想定しにくいエッジケースが、形式仕様を起点としたPBT生成によって自動的に検出される様子が確認できました。
実際のデモの様子は、登壇者が公開している以下の動画で確認できます。
4つの設計判断
spec-to-pbt の開発にあたり、@ohbarye さんが採用した設計判断として4つの方針が紹介されました。
Scaffold, not compiler
形式仕様から Ruby のテストコードへの変換は、コンパイラ的な完全変換ではなく、スキャフォルド（人間が手を入れる前提の叩き台）として実装されています。
理由として、形式仕様は「何が成り立つべきか」を記述するものであり、Ruby 側のメソッド名や引数の型、状態の観察方法といった「どう呼び出すか」までは指定していません。この埋め合わせをツールが推測で行うと、実装に存在しないメソッドを呼ぶテストや、仕様の意図したものとは異なる性質を検証するテストが出力されるリスクがあります。そのため、確信を持って推論できる範囲は生成し、それ以外は設定ファイル側で人間が明示的に書く前提のスキャフォルドを生成するという判断とのことです。
Regeneration-safe output
spec-to-pbt は、テストファイルと設定ファイルを別々に出力する設計を採用しているとのことです。
人間が編集するのは設定ファイル側のみで、テストファイルはツールから何度でも安全に再生成可能です。これにより、形式仕様が変更されたあとにテストを再生成しても、人間の手を入れた内容が失われることはありません。
Fix upstream, not workarounds
spec-to-pbt ではステートフルPBTの生成が必要になりましたが、@ohbarye さんが過去に開発した pbt gem の側にはステートフルPBTの機能が存在していませんでした。
そこで spec-to-pbt 内で代替となる実装を入れるのではなく、pbt gem 本体にステートフルPBTの機能を追加するという判断をされたと紹介されました。pbt gem を作った当時にはユースケースのなかった機能が、spec-to-pbt の開発を通じてユースケースとして浮かび上がった、という気付きについても言及がありました。
Pattern analysis and promotion
決定的にPBTを生成するためには、ツール側で「推測」を行わず、対応関係を1つずつパターンとして対応づけていく必要があります。
ここで難しかったのは、「どのパターンを生成可能と判断するか」を決めることだったとのことです。あるパターンが生成可能であるかを判断するための条件として、以下の5つが紹介されました。
- 異なるドメインに出現する（複数の仕様で再利用される普遍的なパターンか）
- 構造的に仕様本体から推論可能である（ドメイン知識に依存しないか）
- 安全な既定動作を持つ（確信が持てない場合は、テストを断定的に生成せずコメントに留める）
- 実際に設定作業を削減する（自動化しても結局ユーザーが上書きする形になっていない）
- リグレッション範囲を維持する（同じパターンを使う異なる仕様に適用しても、仕様ごとの個別の修正なしにテストが通る）
これらの条件は事前に設計されたものではなく、実際に複数のドメインで spec-to-pbt を試した結果から整理された経験則であることが、リポジトリの retrospective ドキュメントに記されています。
5つの条件を通った例として、コネクションプールのような、ある値を1つ減らすと別の値が1つ増える関係を持つパターンが挙げられていました。
逆に、ビジネスプロセスに深く結びついたものは安全に生成できないと判断され、対象から除外されたとのことです。
現状の制約と今後の展望
spec-to-pbt は現状ではかなり限定的なツールであるとして、対応しているのは既知のパターンのみであること、ステートフルPBT専用でステートレスPBTには未対応であること、生成されるテストコードが読みづらいこと、Alloy のパースが正規表現ベースで構文の一部しかカバーできていないことが挙げられました。今後はパターンの拡充、ステートレスPBTへの対応、テンプレートの簡素化、Alloy Analyzer の AST を用いたより深いパースに取り組んでいきたいとのことです。
セッションの締めくくりでは、人間が形式仕様を書き、spec-to-pbt がそこからPBTを生成し、AI が実装を書く、という将来像が示されました。仕様自体が形式手法によって検証され、実装は生成されたPBTによって検証されることで、より良い品質保証が実現できるのではないか、という見立てです。冒頭で述べられたAI時代の品質保証という問いに対して、形式仕様とPBTを組み合わせる本アプローチが一定の答えを示している、という形でセッションは結ばれました。
Q&A — 形式仕様と生成コードの対応の正しさをどう保証するか
セッション後の質疑応答では、私から以下の質問をさせていただきました。
形式仕様と、そこから生成されたPBTについて、対応が正しいことを検証する構想は将来的にあるか。
@ohbarye さんからいただいた回答の要旨は以下のとおりです。
- 現状のアプローチでは、対応の正しさを検証することは難しいと感じている
- Haskell など他言語の例では、形式仕様から型情報を生成し、型情報からMBT（Model-Based Testing。PBTと近縁の手法）を生成するという、ほぼコンパイルに近い流れが構築されているため、生成されたテストの正しさが保証されやすいと考えられる
- Ruby で同様のアプローチを取る場合、RBS を介して生成するという可能性も検討された
ここから先は、Q&A を踏まえた私自身の解釈になります。
Q&A で出てきた「対応の正しさを検証する手段がまだない」という話は、先述の「Scaffold, not compiler」という設計判断と表裏の関係にあるように感じました。コンパイラ的なアプローチは変換の各ステップに意味保存性を持たせやすいため、生成されたテストの正しさを構成的に保証しやすくなります。一方でスキャフォルド方式は、人間が設定ファイル側で手を入れられる柔軟性を持つ反面、その箇所に揺れが入り込む余地もあり、対応の正しさを機械的に通すことが難しくなります。
今回のアプローチで対応の正しさの検証が現時点では難しいというのは、ツール固有の課題というよりも、人が調整するのを前提として機械側の責任範囲を引いた結果から派生する構造的な性質ではないか、と整理しています。
感想
形式手法とPBTをつなぐ取り組みを、Rubyで実際に動くツールとして見られたのは面白かったです。AI時代の品質保証をどう作っていくかという問いに対する1つの方向性が見え、とても刺激的でした。
生成される scaffold には解析の確信度や推論ヒントがコメントとして埋め込まれており、Scaffold, not compiler という思想が生成物にも一貫して表れているのが印象的でした。
Techouseでは、社会課題の解決に一緒に取り組むエンジニアを募集しております。 ご応募お待ちしております。
