Amazon Web Services ブログ

Kiro : コードは仕様と一致していますか？ 〜プロパティベーステストで「正しさ」を測定する〜

本記事は 2025 年 11 月 17 日に公開された Aaron Eline（Researcher）による “Does your code match your spec?” を翻訳したものです。

仕様の重要性

Kiro は 7 月にローンチした際に仕様駆動開発（Spec Driven Development、以下、SDD）を導入したエージェント型 IDE です。SDD では、Kiro のエージェントがコードを書く前にソフトウェアの完全な仕様を作成します。これにより、開発前にエージェントと繰り返しやり取りしながら、アプリケーションの要件を完全に捉えられているか確認できます。Kiro はその要件ドキュメントを実行して Spec （仕様）に変換し、生成されたコードが仕様に準拠しているかをチェックします。Kiro はこの実行可能な仕様を使ってプログラムをテストしますが、その際にプロパティベーステストと呼ばれる手法を使用します。私たちはこの手法は、バグ発見により効果的であると考えています。

要件からプロパティへ

Kiro を使うと、仕様からコードが生成されます。しかし、そのコードが本当に仕様通りに動作するかをどうやって確認すればよいのでしょうか？Kiro や他の生成 AI コード生成ツールは、この問いに答えるために自動生成されたユニットテストを使ってきました。Kiro はコードと一緒にユニットテストを生成し、コードがそれらをパスすることを確認します。しかし、ここには鶏と卵の問題があります。ユニットテストが仕様で示された動作を捉えているかをどうやって確認するのでしょうか？各テストを見て、1/ そのテストがどの仕様要件に適用されるのか、2/ テストで規定された動作が仕様と一致しているかを判断する必要があります。どちらのステップも面倒でエラーが起きやすい作業です。

実際のところ、ユニットテストの代わりにプロパティベーステストを使用することで、より優れた結果を得られる場合があります。ユニットテストは本質的に「例ベース」のテストで、単一の入力と出力のペアで構成されています。各テストは特定の例において、システムが特定の方法で動作することを主張します。対照的に、プロパティベーステスト（または単にプロパティテスト）は、システムの動作についてプロパティが真であることをテストします。つまり、広範囲の（場合によっては無限の）入力に対してそれが成り立つことを確認します。この普遍性こそが、プロパティテストに力を与えるものです。プロパティテストでは、多くの入力をランダムに生成してテストします。プロパティテストが false を返した場合、そのプロパティを破る反例を見つけたことになります。これはテスト対象のプログラムのバグを表している可能性が高いです（ただし、プロパティ定義のバグや元の仕様のバグである可能性もあり、それを見つけることも有用です）。Kiro はこの例を使って、正しくなるまでコードを修正できます。

プロパティベーステストは 20 年以上前に Haskell プログラミング言語向けに QuickCheck というフレームワークで発明されました。それ以来、成長し成熟してきました。プロパティテストは、Kiro が行うような仕様駆動開発と非常に相性が良いです。なぜなら、仕様要件は多くの場合、直接的にプロパティを表現しており、これらのプロパティはプロパティベーステストを使ってテストできるからです。ある意味で、プロパティは仕様の（一部の）別の表現です。プロパティベーステストを使えば、動かして確認できる仕様表現が手に入ります。プロパティベーステストで構成される実行可能な仕様は、テキストの要件と簡単に結びつけられるため、プロパティテストがパスする限り、コードが要件通りに動作しているという確信が得られます。

例

例として、Python で小さな信号機シミュレーターを書いているとしましょう。Kiro は受け入れ基準で構成される要件ドキュメントを含む仕様を作成します。受け入れ基準の 1 つは次のようになるかもしれません。

要件 2.3: 安全性の不変条件
システムは、矛盾する交通の流れを防ぐために、任意の時点で最大 1 つの方向のみが緑信号を持つことを保証しなければならない。

この基準は、信号機の重要な条件を表現しています。2 つの方向が同時に緑になることは決してないということです。この受け入れ基準をテキストのプロパティに変換すると次のようになります。

プロパティ: 安全性の不変条件 - 最大1つの緑信号
*任意の*操作シーケンス（状態遷移、緊急モードの有効化、タイミング更新）に対して、
任意の時点で、最大1つの方向のみが緑信号を持つべきである
**検証対象: 要件 2.3**

このプロパティが「任意の」という言葉で始まっていることに注目してください。これがプロパティである理由は、単一の例の入力がどう処理されるべきかの説明ではなく、入力と動作の範囲について語っているからです。Kiro はこのプロパティテキストをもとに、実行可能なテストコードへ変換します。Kiro は、テキストの仕様からこのプロパティをチェックするテストへ直接ナビゲートできるようにすることで、両者を結びつけます。

Kiro はテキストのプロパティを、Hypothesis というフレームワークを使って書かれたプロパティベーステストに変換します。これについては後ほど詳しく見ていきます。信号機のプロパティのコードは以下の通りです。このコードを読めば、実際に私たちが気にしているプロパティをチェックしていることがわかります。まず、正常な状態から始まっていることを確認します。次に、操作スケジュールの各操作を反復処理し、それらを適用して、常に 1 つの緑信号しか見られないことを確認します。

def test_safety_invariant_at_most_one_green(
    timing_config: TimingConfig,
    operations: list
):
    """機能: 信号制御システム、プロパティ 2: 安全性の不変条件 - 最大1つの緑信号
    検証対象: 要件 2.3
    """
    # 状態マネージャーと制御モジュールを作成
    state_manager = SignalStateManager(timing_config)
    control_module = ControlModule(state_manager)

    # 初期状態（すべて赤）が安全性を満たすことを確認
    assert control_module.validate_safety(), "初期状態は安全であるべき"

    # 各操作を実行し、操作後に毎回安全性を確認
    for operation in operations:
        op_type = operation[0]

        if op_type == 'transition':
            _, direction, state = operation
            control_module.request_transition(direction, state)
        elif op_type == 'emergency_activate':
            _, direction = operation
            control_module.activate_emergency_mode(direction)
        elif op_type == 'emergency_deactivate':
            control_module.deactivate_emergency_mode()

        # すべての操作後に安全性の不変条件を確認
        all_states = state_manager.get_all_states()
        green_count = sum(1 for state in all_states.values() if state == SignalState.GREEN)

        assert green_count <= 1, (
            f"安全性違反: 操作 {operation} の後に {green_count} 個の緑信号。"
            f"状態: {all_states}"
        )

このプロパティテストの素晴らしい点は、最初に定義した要件を直接テストしていることです。つまり、多くの入力でテストすれば、その要件を満たしていることに高い確信が持てます。さらに重要なのは、その逆も成り立つことです。この関数を失敗させる入力が存在する場合、プログラムは正しくないのです。Kiro はこの特性を積極的に利用します。

プロパティテストの重要な部分は、プロパティテストを実行するための多様な入力をランダムに生成することです。この例では、重要な入力は test_safety_invariant_at_most_one_green に渡される操作の list です。次のセクションでは、この例の文脈で入力生成について説明します。自動入力生成は、ユニットテストに対する重要な利点を提供します。誰かがユニットテストを書くとき（モデルであれ人間であれ）、エッジケースを考慮しようとしますが、自分自身の内部バイアスによって制限されます。ランダム生成を利用することで、見落とされがちなエッジケースやコンポーネント間の相互作用を発見できることがよくあります。Kiro はこの事実を最大限に活用します。

プロパティの典型パターン

プログラムの正しさに関する文献では、よく現れるプロパティの典型的なパターンがあることがわかっています。Kiro はこれらのパターンを認識しており、プロパティを生成する際にそれらを探します。たとえば、二分探索木のようなデータ構造の一般的なプロパティは、実行時の不変条件を維持することです。個々の操作が不変条件を維持することを検証するプロパティを書けます。

# 挿入操作は二分探索木の性質を維持すべき
def bst_insert(tree, input):
    if is_bst(tree):
        tree.insert(input)
        assert is_bst(tree), "木は依然として二分探索木であるべき"
        assert tree.contains(input), "木は入力値を含むべき"

別の一般的なプロパティのパターンは「ラウンドトリップ」で、一連の操作によって開始時の値に戻るというものです。このプロパティは特にパーサーやシリアライザーに有用です。

# パーサーでほぼ常に成り立つべきプロパティ
# 整形してから再度パースすると、同じ式が得られるべき
def parser_correctness(expression):
    assert parse(pretty_print(expression)) == expression

Web API では、削除操作が「冪等」であることを望むことがよくあります。つまり、アクションを 2 回繰り返しても 1 回実行したのと同じ効果になるということです。

def delete_idempotence(orders_list, order_id):
    if order_id in orders_list:
        assert orders_list.delete(order_id) == orders_list.delete(order_id).delete(order_id)

プロパティの設計についてさらに詳しく知りたい場合は、次のブログ記事をお勧めします。Choosing Properties for Property-Based Testing、および How To Specify it [PDF] の論文です。

入力ジェネレーターを使ったプロパティのテスト

プロパティをテストするには、具体的な入力値が必要です。多数の（数百の）多様な値を取得し、バイアスの影響を減らすために、PBT フレームワークは「ジェネレーター」を使用します。これは何らかのランダム性を受け取り、特定の型の入力値を生成する関数です。プロパティベーステストフレームワークのユーザーは、特定のプロパティテストを実行する際にどの入力ジェネレーターを使用するかを指定します。Kiro は生成するプロパティテストに対してこれを自動的に行います。

Hypothesis などの PBT フレームワークには、一般的な型用のジェネレーターが多数付属しており、これらを構成要素として使ってより複雑なジェネレーターを作成できます。Hypothesis フレームワークはジェネレーターをストラテジーと呼び、多くの場合、ストラテジーを変数 st に格納します。整数を生成するストラテジーの例をいくつか示します。

>>> from hypothesis import strategies as st
>>> st.integers().example()
-43489276822011488813107857396380363774
>>> st.integers().example()
1944533851
>>> st.integers().example()
3
>>> st.integers().example()
-6029
>>> st.integers().example()
-3157022535735084108
>>> st.integers(1,500).example()
271
>>> st.integers(1,500).example()
18
>>> st.integers(1,500).example()
20
>>> st.integers(1,500).example()
350
>>> st.integers(1,500).example()
89

Hypothesis には、カスタムデータ型用のより複雑なストラテジーも付属しています。

>>> st.emails().example()
'^3l@s.K.sM'
>>> st.emails().example()
'~g0}XGSf|m$6wOgvEI`e~8h@Z.roDeO'
>>> st.uuids().example()
UUID('ff1fe0e9-c9a7-324d-f04d-c6f7c3fa4059')
>>> st.uuids().example()
UUID('156c8e91-0ad7-24b0-6e59-0e6b6a114e74')
>>> st.complex_numbers()
complex_numbers()
>>> st.complex_numbers().example()
(-inf-infj)
>>> st.complex_numbers().example()
(nan+352724254975j)
>>> st.complex_numbers().example()
0j

小さなストラテジーから複雑なストラテジーを構築することもできます。たとえば、lists ストラテジーは別のストラテジーを引数として受け取り、その引数によって生成されたもののリストを構築します。

>>> st.lists(st.integers()).example()
[297324786, 38]
>>> st.lists(st.integers()).example()
[13158, 3]
>>> st.lists(st.integers()).example()
[17, 27825, -25292, 30419, -8472, -30306, 6151414495842486117, 1264487630263387308, -10877, 1076876455, -10851]
>>> st.lists(st.booleans()).example()
[False, False, False, False, True, False, False, False, True, False]
>>> st.lists(st.booleans()).example()
[False, False, True, True]
>>> st.lists(st.booleans()).example()

Kiro でのプロパティベーステスト

現在、Kiro は要件をテストするために、プロパティチェックコードとジェネレーターの両方を含むプロパティベーステストを自動的に作成します。先ほどの信号機の例に戻ると、Kiro は先ほど見たプロパティチェックコードを生成するだけでなく、メソッドの上に @given アノテーションを追加し、使用したい 2 つの Hypothesis ストラテジーをリストします。

@given(
    timing_config=timing_config_strategy(),
    operations=operation_sequence_strategy()
)
def test_safety_invariant_at_most_one_green(
    timing_config: TimingConfig,
    operations: list
):

以下は、Kiro がこのプロパティのために書いたストラテジーです。このコードは Hypothesis ストラテジーフレームワークを使用して、信号機の遷移シーケンスに対するストラテジーを構築します。このストラテジーが、Kiro が書いた signal_state_strategy などの他のストラテジーを参照していることがわかります。これにより、複数のプロパティテスト間でコードを共有できます。

# 操作シーケンスを生成するストラテジー
@st.composite
def operation_sequence_strategy(draw):
    """制御モジュールに対して実行する操作シーケンスを生成する"""
    operations = []
    num_operations = draw(st.integers(min_value=1, max_value=20))

    for _ in range(num_operations):
        op_type = draw(st.sampled_from(['transition', 'emergency_activate', 'emergency_deactivate']))

        if op_type == 'transition':
            direction = draw(direction_strategy)
            state = draw(signal_state_strategy)
            operations.append(('transition', direction, state))
        elif op_type == 'emergency_activate':
            direction = draw(direction_strategy)
            operations.append(('emergency_activate', direction))
        else:  # emergency_deactivate
            operations.append(('emergency_deactivate',))

    return operations

このテストは、標準的な Python テストフレームワークである pytest とすぐに統合できます。pytest が実行されると、Hypothesis は 100 個のテストケースを生成し、それらすべてがプロパティをパスすることを確認します。

テストの品質にとって、入力生成ストラテジーが実際に多様な入力を生成することが重要です。Tyche というツールを使って、それらの入力と実行時にカバーされるコードを調べることで、どれだけうまくいっているかを評価できます。以下は、ジェネレーターが生成した入力のサンプルで、Tyche が表示してくれるものです。

以下は、プロパティベーステストによって実行されるコードを示す Tyche が生成した視覚化です。50 回の試行後でも、まだ新しいコードパスを探索していることがわかります。

コードカバレッジについて注意点があります。テストスイートの効果を測定する非常に一般的な指標ですが、テスト品質の最終的な判断基準ではありません。コードの行をカバーする（つまり実行する）ことは、その行のすべての動作を網羅したことを意味しません。プロパティテストは網羅的な手法ではないため、プログラムにバグがないことを保証できません。プロパティベーステストが見つけられない反例が常に存在する可能性があります。しかし、私たちは、プロパティベーステストが従来の例ベーステストよりもバグの発見において効果的なツールであり、仕様とテストをより良く結びつけ、プログラムの正しさの問題を具体的で実行可能な仕様の観点から表現するという重要なステップを踏んでいると考えています。

反例と縮小

この記事を終える前に、プロパティベーステストの本当に役立つ最後の機能について話したいと思います。それは縮小です。プロパティテストが失敗すると、プロパティを失敗させる入力、つまり反例が得られます。理想的には、最小限の入力、つまりテストを失敗させた問題の核心を示す小さな例が欲しいところです。巨大な反例には問題とは関係のない余分なデータが含まれている可能性が高いのに対し、最小限の例は、あなた（そしておそらく Kiro エージェント）がプログラムの実際の欠陥を特定し、修復するのに役立ちます。ほとんどのプロパティベーステストフレームワークは、「縮小」と呼ばれるプロセスを通じて最小限の例を提供しようとします。これがどのように機能するか見てみましょう。

探索木に基づく集合を実装しているとしましょう。おそらく次のようなプロパティがあるでしょう。

# プロパティ: 任意の2つの二分探索木を結合すると、
# 適切な二分探索木になるべき
@given(left = trees(), right = trees())
def test_union_maintains_invariant(left, right):
    assert left.union(right).is_bst()

このテストを実行すると、次のような出力が得られるかもしれません。

Falsifying example:
left = Node(lhs=Empty(), rhs=Empty(), value=0)
right = Node(lhs=Empty(), rhs=Empty(), value=0)

しかし、これは実際には Hypothesis が見つけた最初の反証例ではありませんでした。Hypothesis のログを見ると、最初に失敗した反例は実際には次のようなものでした。

Trying example: test_union(
    lhs=Node(lhs=Empty(),
     rhs=Node(lhs=Empty(),
      rhs=Node(lhs=Empty(), rhs=Empty(), value=30),
      value=-111),
     value=-25482),
    rhs=Node(lhs=Node(lhs=Empty(), rhs=Empty(), value=-26344),
     rhs=Node(lhs=Empty(),
      rhs=Node(lhs=Node(lhs=Empty(), rhs=Empty(), value=42),
       rhs=Node(lhs=Node(lhs=Node(lhs=Empty(), rhs=Empty(), value=6076),
         rhs=Empty(),
         value=10768),
        rhs=Empty(),
        value=27223),
       value=121),
      value=-89),
     value=-20602),
)

これはデバッグがより困難なケースです。縮小は、失敗を引き起こし続けることを確認しながら、失敗した入力を体系的に単純化します。この例では、Hypothesis は不要なノードを削除し、整数値を減らし、木構造を単純化して、最小限のケースを見つけました。それは、両方とも値 0 を含む 2 つの単一ノード木です。これにより、複雑な木構造のノイズなしに、核心となる問題、つまり union 操作が重複値を適切に処理していないことが明らかになります。

Kiro がプロパティテストを生成する際、基盤となる PBT フレームワークの縮小機能を活用します。つまり、開発中にプロパティテストが失敗すると、デバッグを大幅に容易にする実用的で最小限の反例が得られます。エージェントはこの最小限の例を使って根本原因をより簡単に理解し、修正を提案でき、仕様、テスト、実装の間に緊密なフィードバックループを作り出します。Kiro が実装は正しいかもしれないが仕様と一致しないことを発見した場合、または AI が生成したコードが自明でない方法で根本的に間違っているように見える場合、Kiro はこれを開発者に提示して選択を求めます。コードを修正するか、仕様を修正するか、PBT を修正するかです。そうすることで、人間の判断と AI および PBT を組み合わせて、実装を開発者の意図により明確に合わせます。

まとめ

Kiro がプロパティベーステストを採用したことで、AI コーディングタスクにおける正しさの考え方が大きく変わります。個々の例をチェックすることから、入力空間全体にわたる普遍的なプロパティを検証することへと移行しています。自然言語の仕様を実行可能なプロパティに自動的に変換し、包括的なテストケースを生成することで、Kiro は AI エージェントと人間の開発者の両方がより信頼性の高いソフトウェアを構築するのに役立つ強力なフィードバックループを作り出します。このアプローチは、従来のテストが見逃すバグを見つけるだけでなく、要件とそれらを検証するテストの間に明確で追跡可能なリンクを維持します。PBT はすべてのバグの不在を保証できませんが、例ベーステストだけよりも大幅に強力な正しさの証拠を提供し、仕様駆動開発にとって不可欠なツールとなっています。

LLM とプロパティベーステストに関する詳細については、以下の研究論文を参照してください。

Kiro をダウンロードして、仕様でプロパティベーステストを試してみてください。

翻訳は AppDev Consultant の宇賀神が担当しました。