BT

InfoQ ホームページ ニュース 純粋関数のプロパティを記述するには - John Hughes氏のLambda Days 2020での講演より

純粋関数のプロパティを記述するには - John Hughes氏のLambda Days 2020での講演より

ブックマーク

原文(投稿日:2020/02/24)へのリンク

HaskellとQuickcheckの共同設計者のひとりであるJohn Hughes氏が、先日のLamdba Days 2020で、プロパティ(property/特性)ベースのテストについて論じた。講演の中で氏は、プロパティを導入するための5つの戦略を紹介し、それぞれの効率性を比較した上で、結論としてメタモルフィック(Metamorphic)プロパティとモデルベースプロパティが高い効率性を見せたことを報告した。

最初にHughes氏は、純粋関数(pure function)のテストにPBT(property-based testing)を使用する開発者が直面する、共通的な問題について論じた。EBT(example-based testing)では、テスト時に期待される関数の出力を事前に計算して、関数の実際の出力と比較することができる。これに対してPBTでは、ランダムに近い多数のテストシーケンスが生成されるのが一般的だ。事前に分からない多数の値に対して、テスト時に期待される関数の出力を計算するというのは、最初に関数を実装する時と同じ位の困難を伴う作業である。この課題はテストオラクル問題(test oracle problem)と呼ばれるものだ。Tsong Yueh Chen博士が次のように説明する。

オラクル問題とは、与えられたテストケースのテスト結果の検証が極めて困難か、あるいは不可能な状況を示すものです。

このため、オリジナルのコードがそのままテストで使用される場合があり、テスト対象コードと同じバグをテスト実施コードに持ち込む結果になる。

この難問を解決するためにHughes氏は、テスト時に関数出力のプロパティを特定し、チェックすることを推奨する。指定されたリストを逆順にして返すreverseという関数のプロパティのひとつは、次のようなものになる。

reverse (reverse xs) === xs

問題なのは、バグを見つけるか、あるいは関数実装が適切であることを確認する上で、適切なプロパティセットを見つけることだ。Hughes氏はここで、次のような不適切な"reverse"の実装を例として、ひとつだけのプロパティでは不十分であることを示してみせた。

reverse xs = xs

次にHughes氏は、プロパティを生成するための5つの体系的な方法を示して、それらの有効性を分析した。最初の方法は、テスト対象の関数の不変条件(invariant)を特定することだ。この方法を説明するために、Hughes氏は、findinsertdeleteunionというオペレーションを持つバイナリ検索ツリー(BST)データ構造を例にあげた。このデータ構造には、有効なツリーにキー/バリューペアを挿入(insert)することで、結果として有効なツリーが得られるというプロパティがある。削除(delete)や結合(union)操作についても、これと同じプロパティが適用される。ツリー自体は、バイナリ検索ツリーの規約(特にキーの順序を参照する規約)に準拠していれば、有効であると判断される。

第2の方法は、テスト対象の関数の出力によって検証される事後条件(postcondition)を見つけることだ。例としてHughes氏は、BSTのfind操作に関する次のような事後条件をあげた。

insertコール後、挿入されたキーと、それ以前に存在した任意のキーをfindで検索できなければならない。

第3の方法は、メタモルフィックプロパティに関するものだ。メタモルフィックプロパティは、関連性のある入力に対してテスト中のシステムが生成した出力を関連付ける、という方法だ。

insert k v (insert k' v' t)
===
insert k' v' (insert k v t)

このプロパティは、2組のキー/バリューを挿入した結果のツリーが挿入の順に依存しない、という単純なものだ。メタモルフィックテストは現在、積極的に研究されている分野である。このテクニックに関する詳細な研究は、Tsong Yueh Chen教授の論文"Metamorphic testing: A review of challenges and opportunities"に見ることができる。

4番目の方法は、Hughes氏の言う帰納的プロパティ(inductive properties)に基くものだ。シニアソフトウェアアーキテクトのScott Wlaschin氏が、PBTでの講演で、次のように説明している。

この種のプロパティは、構造的機能法(structural induction)に基いています。つまり、大きなものが小さなパーツに分解可能で、なおかつ分解したパーツそれぞれのあるプロパティが真であれば、大きなものについてもそのプロパティが真であると証明できる場合が多い、ということです。(…)
帰納的プロパティはリストやツリーといった再帰的な構造に対して、多くの場合において無理なく適用されます。

Hughes氏は、BSTに次のような帰納的プロパティを定義した。

union nil t ==== t
union (insert k v t) t'
=~= 
insert k v (union t t')

要するにこれは、ツリーに対するunion操作が、ツリーの一部に対するunion操作に関連付けられる、という意味だ。ツリーのサイズに対する帰納法によって、これらのプロパティを満足する関数のみがBSTの正しいunion操作である、ということを示すことができる。帰納的プロパティはそれ自体がメタモルフィックプロパティであることが多く、完全な仕様を形成し、帰納的証明にリンクされているという特徴を持っている。

第5の方法はモデルベースのプロパティによるものだ。この方法では、テスト対象とするシステムのモデルが存在することが前提となる。BSTの例では、単純なモデルはツリーに格納されたキーバリューのリストであり、ツリーデータ構造を走査することによって獲得できる。テスト対象のシステム上のオペレーションは、モデル上のオペレーションへと転換され、データ構造のプロパティのチェックは、モデルのプロパティのチェックに置き換えられる。これは、後者のチェックの方が非常に単純である、あるいは信頼性の高い方法での実行が容易である、という考えに基くものだ。

それぞれのプロパティの有効性を評価するためにHughes氏は、正しいBST実装のすべての操作にバグを紛れ込ませて、それぞれのプロパティ生成方法で見つかったバグをカウントした。

 

プロパティのタイプ プロパティの数 有効性
不変条件 4 38%
事後条件 5 79%
メタモルフィック 16 90%
モデルベース 5 100%

 

モデルベースプロパティの有効性は100パーセントに達しており、テスト対象のシステムに関するオラクルの把握に最も近い位置にある。この場合のモデルは、オラクルを利用可能なテスト対象システムの簡略版として機能する。メタモルフィックも、バグ検出においては大きな効果がある。さまざまな業界での結果も、これと一致している。"Metamorphic Testing: A Review of Challenges and Opportunities"でも取り上げられているように、メタモルフィックテストの大きな功績は、有名な2つのコンパイラ(GCCとLLVM)の100を越えるバグを新たに検出したことだ。

講演に関する論文の中でHughes氏は、次のような妥当な結論を下している。

これらの結果から、時間に制限のある場合には、モデルベースのプロパティを記述して、無効なデータによって発生するエラーによる混乱を避けるために有効性(validity)プロパティと組み合わせるという方法が、所要時間に対して最も大きな結果を得られると思われます。モデルの定義が複雑(で時間を要する)場合、あるいはモデルが実装に極めて近いため同じバグが発生する可能性が高い場合には、記述するプロパティの数は多くなりますが、メタモルフィックプロパティが効果的な代替策になるでしょう。

Lambda Days 2020の講演を記録したビデオがオンラインで公開されている。Lambda Daysは関数プログラミングの手法とテクニックに特化した開発者向けカンファレンスで、Lambda Day2 2020は2020年2月13,14の両日、ポーランドのクラクフで開催された。

この記事に星をつける

おすすめ度
スタイル

こんにちは

コメントするには InfoQアカウントの登録 または が必要です。InfoQ に登録するとさまざまなことができます。

アカウント登録をしてInfoQをお楽しみください。

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

コミュニティコメント

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

BT

あなたのプロファイルは最新ですか?プロフィールを確認してアップデートしてください。

Eメールを変更すると確認のメールが配信されます。

会社名:
役職:
組織規模:
国:
都道府県:
新しいメールアドレスに確認用のメールを送信します。このポップアップ画面は自動的に閉じられます。