QuickCheck 最初の一歩リストの逆順を写経

まずは写経。

準備としては、Quviq のサイトから eqc mini を落としてきて適当な場所に解凍するだけです。

http://www.quviq.com/news100621.html

最初の題材は、 Hughes さんのトーク

Functional Programming: A Secret Weapon for Software Testing.
John Hughes gives an invited talk at ICFP 2007 in Freiburg, Germany, showing from his company's experience how QuickCheck has found many obscure bugs in commercial software. *Even when the software under test is not written in a functional language.*
hughes_testing

のなかにある、リストの逆順操作。

単純すぎる例かもしれないけれど、連結操作との交換(といっていいのかな?)で逆順を定義する、というのはとてもシンプル。ちゃんと考えていないけど、これだけで帰納的に操作が定まっているのではないかと思う。

-module(first_samples).

-include_lib("eqc/include/eqc.hrl").

-export([start/0]).

%% 写経
%% http://video.google.com/videoplay?docid=4655369445141008672#

start() ->
  eqc:quickcheck(prop_reverse_combination_mistake()),
  ok.

%% こっちは失敗する。失敗入力がシュリンクされる
prop_reverse_combination_mistake() ->
  ?FORALL({Xs, Ys},
          {list(int()), list(int())},
          lists:reverse(Xs ++ Ys) =:=
            lists:reverse(Xs) ++ lists:reverse(Ys)).

コンパイル。

erlc -I ../eqc-1.0.1/include -pa ../eqc-1.0.1/ebin first_samples.erl

実行

$ erl -pa ../eqc-1.0.1/ebin -pa . -s first_samples -s init stop -noshell
Starting eqc mini version 1.0.1 (compiled at {{2010,6,13},{11,15,30}})
.................Failed! After 18 tests.
{[2,-2],[-5]}
Shrinking....(4 times)
{[0],[1]}

アウチ。こけました。まぁコメントに書いてますね。
前回書いた、QuickCheck の手順を再掲。

入力をたくさん勝手に生成して、
何か処理したあとに、
不変性などのチェックを行う。
そしてチェックが失敗したら、
入力をなるべく簡略化して失敗する入力を教えてくれる。

まず、実行結果2行目の Failed! までで、勝手に入力を生成してテストをしています。

「何か処理」と「チェック」はコードの prop_reverse_combination_mistake の中にあります。?FORALL マクロの第3引数がそこ。ただし簡単なので「何か処理」ってのは無く、すぐに性質(プロパティ)のチェックを行っています。

そして、18 テストをしたあとに失敗しました、と報告してくれています。その時の入力が

{[2,-2],[-5]}

の部分です。

この後に、入力を簡略化して、なにがおかしいのかを人間に分かりやすくしてくれるプロセスが走ります。 Srinking.. とあるところです。結果として、入力のリストは1要素だけのリストであれば良い、という結果を出力しています。
このケースではそもそも結果が複雑ではありませんが、実際には重要なステップとなるところでしょう。このシュリンクするロジックも気になりますね。どうなってるんだろう。

本来であれば、ここで実装側のバグなのか、性質の定義がおかしいのかを判断するところです。今回は性質の定義が間違っているため、修正して正しい性質にします。

%% こっちは正しい性質
prop_reverse_combination() ->
  ?FORALL({Xs, Ys},
          {list(int()), list(int())},
          lists:reverse(Xs ++ Ys) =:=
            lists:reverse(Ys) ++ lists:reverse(Xs)).

比較の右辺で、入力のリストが逆になっているところがミソですね。

erl -pa ../eqc-1.0.1/ebin -pa . -s first_samples -s init stop -noshell
Starting eqc mini version 1.0.1 (compiled at {{2010,6,13},{11,15,30}})
....................................................................................................
OK, passed 100 tests

テストが通りました。

日本語で書くと、ここで検証した「逆順(L)」という操作の性質(プロパティ)は、次のようなかんじでしょうか。

任意のリスト L に対して、それを任意に分割したサブリスト L = L1 + L2 が

逆順(L) = 逆順(L2) + 逆順(L1)

を満たす。

入力を L1, L2 (Xs, Ys) ではなく、L 自体にしてプロパティを書きなおしてみます。ちょっと煩雑になりますが、このように FORALL マクロを繋げたり、ステートメントをブロック化して、性質の検証前にちょっとした「何か処理」をすることが出来ます。

prop_reverse_combination2() ->
  ?FORALL(L, list(int()),
  ?FORALL(I, choose(0, length(L)),
          begin
            {L1, L2} = lists:split(I, L),
            lists:reverse(L) =:=
              lists:reverse(L2) ++ lists:reverse(L1)
          end)).

list() とか choose() あたりを調べるには、Quviq のトレーニングを受けるのが正当なんでしょうけど、ひとまず次のような調べ方があります。

eqc.hrl の define とか import を見て推測する。
triq ( https://github.com/krestenkrab/triq )の README を読む。
本家 Haskell の QuickCheck のドキュメントを読んで、Erlang に翻訳する。

まぁどれもいきあたりばったりですね。eqc mini にはドキュメントはほぼありません。

続く、かもしれない。