2008-10-14 [長年日記]
λ. SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values
SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values. Colin Runciman, Matthew Naylor and Fredrik Lindblad. in Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell
を読んだ。
QuickCheck がランダムテストなのに対して、SmallCheck は指定した上限までの範囲の網羅的な検査を行う*1。 QuickCheckでは値が適切に分散するように値の生成機を書くのは簡単ではないが、SmallCheckでは確率を考えながらパラメータをいじったりする必要がない。 また、QuickCheckでは発見された反例は最小のものとは限らないが、SmallCheckは小さいものからテストするので常に最小の反例が見つかる。
SmallCheck は網羅的なテストであるためあまり深い範囲の検査は難しいという問題がある。プロパティの持つ非正格性を利用してそれを解決しようとしているのが Lazy SmallCheck で、データ構造の一部に⊥を含む値をテストの入力として与える。結果がTrueやFalseであれば、⊥の部分を具体的な値にrefineしてもその結果は変わらないはずなので、多くの値に対するテストを省略できる。結果が未定義(エラー)であれば、⊥の部分をより具体的な値にrefineしていく。
それから、Lazy SmallCheck はプロパティの条件部に使うために並列論理積(parallel conjunction)を提供しているのが面白かった。条件部で通常の論理積の代わりに並列論理積を使うことで、生成された値に対する条件の検査結果を未定義(エラー)からFalseにすることが出来場合があり、その場合にはその値をrefineするような値の生成を省略することが出来る。
関連
- <URL:http://www-users.cs.york.ac.uk/~mfn/lazysmallcheck/>
- <URL:http://video.google.com/videoplay?docid=8540922190337591178>
- <URL:http://jp.citeulike.org/user/msakai/article/3406980>
*1 背景には Daniel Jackson の small scope hypothesis という仮説がある