Kiro で始める Property-Based Testing：想定外を炙り出す

これは豆蔵デベロッパーサイトアドベントカレンダー2025第17日目の記事です。

プロパティベーステスト（以下 PBT）は、仕様から抽出された「満たすべき性質（property）」を任意の入力・状態・操作系列に対して検証するテスト手法です。PBT は、従来の事例ベーステストと相互補完的な関係にあることが知られています^[1]。

正直、この説明だけでピンと来る人は多くないのではないでしょうか。私自身も、以前から興味はあったものの、満たすべき挙動の形式化が難しい、実装コストが高そうと感じて手を出せずにいました。

しかし、2025年11月17日に GA となった Kiro では、IDE 機能として 「プロパティベーステストによる仕様の正確性検証」 が導入されました^[2]。この新機能により、PBT 導入のハードルが下がったように見えたため、実際に手を動かして体験してみることにしました。

Kiro の PBT 機能については、公式ドキュメント「Correctness with Property-based tests」を参照してください。

書籍『実践プロパティベーステスト』^[3]では、PBT の特徴を次のように説明しています。

テストのための例をたくさん書いたり、コードに投げるためのランダムなデータを生成したりするのではなく、コードに潜む思いもよらなかった新しいバグを見つけるための手法である

具体例で考えてみましょう。従来の事例ベーステスト（EBT）では「1 と 3 を足したら 4 になる」のような特定の例を確認します。一方 PBT では「どんな数字を 2 つ足しても、順番を変えて足した結果と同一になる」という普遍的な性質を定義します。

左図は EBT、右図は PBT のイメージです。EBT はテストケースを手動で作成し検証する一方、PBT はプロパティを定義してランダムな入力で検証します。

つまり、EBT は予測可能なバグに強く、PBT は予測できなかったバグを発見できる可能性があります。この違いは、後半の UI 表示テストで実感することになります。

Kiro + PBT の解説記事として、「部屋移動ゲーム」を題材にした Medium 記事^[4]があります。

このゲームは、以下の構造により PBT に非常に向いています。

状態 × 操作 × 不変条件（Property）

同じ構造は、 業務アプリケーションにも頻出すると考え、
今回はその一例である、「チケット管理」を題材とすることにしました。

チケット管理には以下の特徴があります。

• 状態遷移の制約
• 終端状態の不変条件
• 再実行・順序依存性
• 異常系の保証

これらは 事例ベーステストでは拾いにくいが、PBT と相性が良い性質です。
そのため、実務への応用を意識してチケット管理を題材に選びました。

今回は、あえて仕様を極限まで単純にしました。

Status = { Open, InProgress, Done }

• 上記の３つのみ

Open        → InProgress
InProgress  → Done

• 上記以外の遷移はすべて無効
• Done は終端状態であり、どの操作も受け付けない

この最小仕様を、Kiro に入力していきます。

まず、Kiro IDE に以下の要件を入力します。

- GUI ベースの簡易チケット管理アプリを作成する
- 永続化は不要、検証用の最小アプリとする
- チケットは必ず3状態のいずれかを持つ
- 状態は「未対応→対応中→完了」の一方向のみ遷移可能
- 完了状態から他状態へは遷移できない
- 状態更新はボタン押下で切り替える
- 機能は作成・一覧・状態更新に限定
- 状態遷移ルールを不変条件として PBT で検証したい

以下のような要件文書が出力されました。
受入基準が EARS 記法^[5](「Easy Approach to Requirements Syntax: 要件定義の構文ルール)で明確に言語化されています。

### 要件3

**ユーザーストーリー:** ユーザーとして、チケットの状態を更新したい。作業の進捗を正確に反映するため。

#### 受入基準

1. WHEN ユーザーが未対応チケットの状態更新ボタンを押した時 THEN Ticket_System SHALL そのチケットを対応中状態に変更する
2. WHEN ユーザーが対応中チケットの状態更新ボタンを押した時 THEN Ticket_System SHALL そのチケットを完了状態に変更する
3. WHEN チケットが完了状態の時 THEN Ticket_System SHALL 状態更新ボタンを無効化する
4. WHEN 状態遷移が実行される時 THEN Ticket_System SHALL 未対応から対応中、対応中から完了の順序のみを許可する
5. WHEN 完了状態のチケットに対して状態変更が試行された時 THEN Ticket_System SHALL その操作を拒否し現在の状態を維持する

特に注目したのは、無効な遷移は拒否される、完了状態では操作できない、状態遷移の順序制約といった 後続の Property 定義につながる記述が明確になっていた点です。

設計書生成時、Kiro は次のことを宣言しました。

設計文書の前半部分を作成しました。次に、受入基準の分析を行ってから正確性プロパティを定義します。

出力結果の抜粋は以下でした。
Property が設計成果物として明示的に出力されています。

### プロパティ1: チケット作成時の初期状態
*任意の*有効なタイトルに対して、新しいチケットを作成すると、そのチケットは常に未対応状態で作成される

### プロパティ2: チケット作成時のリスト追加
*任意の*チケットリストと有効なタイトルに対して、新しいチケットを作成すると、リストのサイズが1増加し、新しいチケットがリストに含まれる

### プロパティ3: チケット表示内容の完全性
*任意の*チケットに対して、そのチケットをレンダリングした結果には、タイトルと現在の状態情報が含まれる

### プロパティ4: 有効な状態遷移の実行
*任意の*チケットと有効な遷移（未対応→対応中、対応中→完了）に対して、状態更新操作を実行すると、チケットの状態が期待される次の状態に変更される

### プロパティ5: 無効な状態遷移の拒否
*任意の*チケットと無効な遷移に対して、状態更新操作を実行しても、チケットの状態は変更されない

### プロパティ6: 完了状態での操作無効化
*任意の*完了状態のチケットに対して、状態更新ボタンは無効化され、操作が実行できない

### プロパティ7: システム不変条件の維持
*任意の*操作（作成、状態更新）の実行後、システム内の全てのチケットは有効な状態（未対応、対応中、完了のいずれか）を持つ

結果として、状態遷移だけでなく、初期状態の不変性、表示内容の完全性、システム全体の不変条件など、人が明示的に頼んでいない Property まで含めて 7 件が定義されました。

以下のような実装計画が出力されました。

- [ ] 2. ビジネスロジック層
  - [ ] 2.1 状態遷移ロジックのテスト作成
    - **プロパティ4: 有効な状態遷移の実行** (要件 3.1, 3.2, 3.4)
    - **プロパティ5: 無効な状態遷移の拒否** (要件 3.5, 4.2)
    - _要件: 3.1, 3.2, 3.4, 3.5, 4.2_
  
  - [ ] 2.2 状態遷移関数の実装
    - 有効な遷移の判定ロジック
    - 状態更新処理の実装
    - テスト実行と通過確認
    - _要件: 3.1, 3.2, 3.4, 3.5_

tasks.md では、Property、要件、テスト、実装タスクが対応付けられており、「なぜこのテストが存在するのか」 が追跡可能になっていました。

また、TDD によるテストファーストの原則を採用したため、以下の流れが自然に形成されています。

テスト作成 → 実装

TDDを用いたAI駆動開発については、以下の記事も参照してください。

状態遷移の Property は、fast-check^[6] を用いた PBT として実装しました。

記述されたテストコードサンプルを提示します。任意のタイトル、任意の有効状態に対して、遷移の性質が必ず成立することを検証しています。

test('未対応から対応中への遷移が正しく実行される', () => {
  fc.assert(
    fc.property(validTitleArb, (title) => {
      const ticket: Ticket = {
        title,
        status: TicketStatus.PENDING
      };

      // 未対応から対応中への遷移は有効
      const isValid = isValidTransition(ticket.status, TicketStatus.IN_PROGRESS);
      const nextStatus = getNextStatus(ticket.status);

      expect(isValid).toBe(true);
      expect(nextStatus).toBe(TicketStatus.IN_PROGRESS);
    }),
    { numRuns: 100 }
  );
});

完成した画面にいくつかチケットを登録したり、エラーを発生させてみて、動作確認を行いました。

正直に言うと、状態遷移だけでは PBT の凄さは分かりにくいと感じました。
今回の状態遷移のルールは単純なため、事例ベーステストでも十分に確認できてしまうからです。

しかし、UI 表示に関する Property で状況が一変します。

チケットタイトル表示の Property テストでは、
連続する空白が HTML によって正規化されることや、
前後の空白・空白のみのタイトルの扱いが曖昧であることなど、
仕様として意識していなかった問題が検出されました。

これらは、手動テストや事例ベーステストでは、まずテスト観点として挙がらなかったと思います。

この経験から、PBT の価値は「網羅的に試すこと」ではなく、
「人が想定していなかった入力や前提を炙り出すこと」
にあると実感しました。

Kiro を使うことで、以下のことを実感しました。

• PBT 導入の心理的・実装的ハードルは確実に下がった。
• Property を中心に仕様・設計・テストをつなげられる。

今回は単体レベルでしたが、
結合テストやシステムテストでの活用も価値がありそうです。

今回使用したリポジトリは以下で公開しています。
（予告なく公開停止する可能性があります）