Hypothesisから学ぶ「ダイ・ハード」で生き残る方法

以下の文章はこちらの記事を翻訳したものです。

映画『ダイ・ハード3』（原題："Die Hard with a Vengeance"）には、主人公ジョン・マクレーン（ブルース・ウィリス演）とゼウス・カーバー（サミュエル・L・ジャクソン演）が爆発を防ぐために仮説を立てて問題を解決する有名なシーンがあります。彼らは3ガロンと5ガロンの容器を使い、正確に4ガロンの水を計測する必要がありました。

（動画のタイトルが「Die Hard 2」になっていますが、正しくは「Die Hard 3」です。）

この問題は、TLA+などの形式仕様言語を使用して解くことができます。形式仕様言語は、システムの動作を定義するために用いられるプログラミング言語の一種です。これは通常のプログラミング言語と異なり、システムの動作をより厳密で数学的なアプローチで記述することができます。これにより、システムの動作に関するより効果的な推論が可能になります。

最近、Hacker NewsでのTLA+に関する議論で、『ダイ・ハード3』の問題をTLA+を使って解く方法を紹介する面白くて簡単な例へのリンクが見つかりました。この例を理解するために、Leslie LamportのTLA+ビデオコースの最初の2講義を視聴することが役立ちました。この過程で、プロパティベースドテスト、特にHypothesisというコンセプトを思い出しました。

プロパティベースドテストは、コードの振る舞いを高レベルで記述し、その振る舞いが適切であるかを検証するために自動的にテストケースを生成するテスト手法です。これは、従来のユニットテストと異なり、特定の入力と出力を手動で指定する代わりに、コードが一定のプロパティを満たすかどうかを確認します。このアプローチにより、より広範な入力セットに対してコードの正確性を確認することができます。

Hypothesisを用いた『ダイ・ハード』問題へのアプローチ

Hypothesisは、Pythonにおけるプロパティベースドテストにおいて優れた実装を提供しています。このツールを使用して、『ダイ・ハード』の問題を定義することを考えました。

Hypothesisはステートフルテスティングに対応しており、これを利用してTLA+の例をPythonに簡単に移植できることが分かりました。ステートフルテスティングは、テスト中にシステムの状態を追跡し、その挙動を検証する手法です。この方法により、『ダイ・ハード』の問題を効率的に表現し、解決することができました。

from hypothesis import note, settings
from hypothesis.stateful import RuleBasedStateMachine, invariant, rule

class DieHardProblem(RuleBasedStateMachine):
    small = 0
    big = 0

    @rule()
    def fill_small(self):
        self.small = 3

    @rule()
    def fill_big(self):
        self.big = 5

    @rule()
    def empty_small(self):
        self.small = 0

    @rule()
    def empty_big(self):
        self.big = 0

    @rule()
    def pour_small_into_big(self):
        old_big = self.big
        self.big = min(5, self.big + self.small)
        self.small = self.small - (self.big - old_big)

    @rule()
    def pour_big_into_small(self):
        old_small = self.small
        self.small = min(3, self.small + self.big)
        self.big = self.big - (self.small - old_small)

    @invariant()
    def physics_of_jugs(self):
        assert 0 <= self.small <= 3
        assert 0 <= self.big <= 5

    @invariant()
    def die_hard_problem_not_solved(self):
        note(f"> small: {self.small} big: {self.big}")
        assert self.big != 4

# The default of 200 is sometimes not enough for Hypothesis to find
# a falsifying example.
with settings(max_examples=2000):
    DieHardTest = DieHardProblem.TestCase

このファイルに対してpytestを呼び出すと、すぐに解決策が見つかります。

self = DieHardProblem({})

    @invariant()
    def die_hard_problem_not_solved(self):
        note("> small: {s} big: {b}".format(s=self.small, b=self.big))
>       assert self.big != 4
E       AssertionError: assert 4 != 4
E        +  where 4 = DieHardProblem({}).big

how-not-to-die-hard-with-hypothesis.py:17: AssertionError
----------------------------- Hypothesis -----------------------------
> small: 0 big: 0
Step #1: fill_big()
> small: 0 big: 5
Step #2: pour_big_into_small()
> small: 3 big: 2
Step #3: empty_small()
> small: 0 big: 2
Step #4: pour_big_into_small()
> small: 2 big: 0
Step #5: fill_big()
> small: 2 big: 5
Step #6: pour_big_into_small()
> small: 3 big: 4
====================== 1 failed in 0.22 seconds ======================

解説

ここでは、コードとテスト結果は比較的理解しやすいものですが、その内容を簡単に説明しましょう。

まず始めに、2つの空のジャグを持つステートマシンを初期状態として設定します。このステートマシンには、複数の状態遷移が可能であり、それらはrule()デコレータを使って定義されています。

次に、システムが常に守るべき不変条件（invariants）を設定します。「physics_of_jugs」という最初の不変条件は、ジャグに含まれる水の量が現実的な範囲内にあることを保証します。例えば、5ガロンを超える水を保持できる大きなジャグのような、物理的に不可能な状況は排除されます。

次の不変条件「die_hard_problem_not_solved」では、大きなジャグにちょうど4ガロンの水が入る状態を達成しないと宣言します。Hypothesisは、ステートマシンがこの不変条件に違反する可能性があるかどうかを徹底的にテストします。これにより、「ダイ・ハード」問題の解決策をHypothesisが見つける可能性があることが示されています。

要するに、このコードはHypothesisを使用して「ダイ・ハード」問題をプログラム的に解決する方法を示しており、不変条件を設定することでシステムの状態の論理的整合性を保証しています。

Hypothesisの動作原理については、プロパティベースのテスト手法を要約しています。基本的にHypothesisは、指定されたプログラムのプロパティ（ルール、不変条件、データ型、関数のシグネチャなど）に基づいて、プログラムの振る舞いをテストするためのデータやアクションを生成します。プログラムがこれらのプロパティを違反するようなデータやアクションが見つかると、Hypothesisはその問題を最小の例まで絞り込みます。これにより、コードに問題がある場合、その問題が発生するまでの最小のステップを特定できます。

この場合、Hypothesisの出力は「die_hard_problem_not_solved」という不変条件を違反したことを示し、その方法を最小の再現例として提示しています。この再現例は、「ダイ・ハード」の問題の解決策を実際に示しており、映画のキャラクターであるマクレーンとカーバーが問題を解決する方法と一致しています。

Hypothesisはこのようにしてプログラムの振る舞いをさまざまな状況でテストし、特定のプロパティが保持されているかどうかを確認します。これは、バグの特定やソフトウェア品質の向上に非常に役立ちます。特に複雑なロジックや条件を持つプログラムでは、このようなテストが不可欠です。

まとめ

TLA+の例をPythonに移植してHypothesisを使ってみた結果、非常に感動しました。Hypothesisが解決策を導き出した瞬間は、思わず笑みがこぼれました。コンピュータが問題解決のプログラムを実際に生成する様子を目の当たりにするのは、本当に素晴らしい体験です。さらに、「ダイ・ハード」の問題をPythonで記述した場合、TLA+のオリジナルと比べてもそれほど冗長ではないことが分かりました。ただし、TLA+での現在値と次の値を示す表現（例えば、small と small'）は非常に洗練されており、old_small や old_big といった変数を使わなくて済む点が優れていると感じました。

HypothesisとTLA+を一般的に比較する知識はまだ持ち合わせていませんが、プロパティベースのテストやTLA+についての学びは始まったばかりです。これらの手法が、データエンジニアリングの現場でどのように活用できるかに大きな興味を持っています。データエンジニアリングでは、プロパティベースのテストや形式的な仕様記述言語（TLA+のようなもの）が、データ品質やデータ処理パイプラインの信頼性を高めるのに役立つ可能性があると考えています。

この小さな実験が楽しかったこと、そして新しい知識を得ることへの意欲が素晴らしいことは間違いありません。この投稿のドラフトを読んでフィードバックをくれたJulia、Dan、Laura、Anjana、Cipに感謝の気持ちを表します。