QuickCheck / SmallCheck の紹介 〜オートマトンの例を通して〜 konn-san.com

QuickCheck を使ってみる

理屈の上では多分二番目のも素朴なaDivBy6’と同様に動いてくれる筈です．でも，ちょっと不安だなあ……． と云うわけで，早速 QuickCheck で確かめてみましょう！

6で割れればaDivBy6でその二進数表現が受理される，と云う条件を書きます．

showBin :: Integral r => r -> String
showBin = flip (showIntAtBase 2 intToDigit) ""
   
test_automaton0 :: Word -> Automaton Int Char -> (Word -> Property)
test_automaton0 base auto = \r -> r `mod` base == 0 ==> isAccepted auto (showBin r)

showBin は2進表現に変換するヘルパ函数ですね． test_automaton0は，底とチェックしたいオートマトンを受け取って，仕様を返す函数です． QuickCheck での「仕様」は，単なるBoolかProperty，または何らかの引数を取ってBool または Propertyを返す函数のいずれかです．わかりやすいように，ここでは仕様になる部分を括弧で括って

Word -> Property

と書いています．何らかの引数，と云いましたが，正確には QuickCheck が生成方法を知っている必要があるので，Arbitraryクラスのインスタンスであるひつようがあります．ここではWord，すなわち正の整数です． なので，これは，「指定した底で割り切れるならオートマトン auto で受理される」のが仕様です．

では，実際にテストしてみましょう！テストするには，quickCheck函数に喰わせるだけで大丈夫です．ライブラリが自動的に例を乱数生成して，仕様が満たされているかチェックしてくれます．

ghci> quickCheck $$ test_automaton0 6 aDivBy6
+++ OK, passed 100 tests.

なんだか矢鱈時間が掛かりますね……．今回は上手くいきましたが，何度か試してみると……

ghci> quickCheck $$ test_automaton0 6 aDivBy6
*** Gave up! Passed only 92 tests.

のように，92の試験に合格したのちに，100に到達しきれなくてギブアップしてます． これは，6の倍数以外も全部生成して試しているからです．事前条件に引っ掛からなかった値は捨て去られるので，大量の無駄が発生してしまっているのです．

では，最初から6の倍数だけ生成して試すようにしてみましょう．

divisible :: Word -> Gen Word
divisible d = (d *) <$$> arbitrary `suchThat` (<(maxBound `div` d))
   
test_automaton1 :: Word -> Automaton Int Char -> Property
test_automaton1 base auto = forAll (divisible base) $$ \r -> isAccepted auto (showBin r)

divisibleで任意の自然数で割り切れる数だけを生成しているわけです．「d 倍しても桁溢れしない任意の数を用意して，それを d倍する」と，そのまま読み下せますね． test_automaton01のほうも，そのまま「任意のbaseで割り切れる自然数 r について，その2進表現が auto で受理される」と読めます．

使ってみると……

ghci> quickCheck $$ test_automaton1 6 aDivBy6
+++ OK, passed 100 tests.

こんどはすぐにテストをパスしています！上手くいったようですね．

と，思いますが，よくよく考えたら問題は「6の倍数か判定するオートマトン」，つまり「6の倍数だけを受理するオートマトン」を作ることでした．このままだと，6の倍数が受理されることはわかりますが，6の倍数でないものが受理される可能性があります．

ではどうするか．折角定義した divisibleを使うのをやめて，両方の場合を一気にチェックする函数に書き換えましょう．

test_automaton2 :: Word -> Automaton Int Char -> (Word -> Bool)
test_automaton2 q a =
  \r -> if r `mod` 6 == 0
        then isAccepted a (showBin r)
        else not $$ isAccepted a (showBin r)

仕様はPropertyでもWord -> Propertyでもなく，単なる述語Word -> Boolに変わっていますね．6で割れれば受理され，そうでなければ受理されないこと，とそのまま記述しています．

では，これを使ってみましょう．

ghci> quickCheck $$ test_automaton2 6 aDivBy6
+++ OK, passed 100 tests.

すぐに実行がおわって，テストを通過しました！やりましたね！

SmallCheck で書いてみよう

では，今度はSmallCheck で書いてみます．と云っても，やることは殆んどかわりません． QuickCheck をインポートしている部分を

import Test.SmallCheck
import Test.SmallCheck.Series

に書き換えて……

test_automaton2 :: Int -> Automaton Int Char -> (N Int -> Bool)
test_automaton2 base auto =
    \(N r) ->
      if r `mod` base == 0
      then isAccepted auto (showBin r)
      else not $$ isAccepted auto (showBin r)

とするだけです！殆んど変更になっていません！

WordがN Intになっていますね．SmallCheck は Word 型をサポートしていないかわりに，Num 型を N でラップしてやることで，正数しか生成しないようになります．

では，早速試してみましょう．

ghci> smallCheck 1000 $$ test_automaton2 6 aDivBy6'
Depth 0:
    Completed 1 test(s) without failure.
Depth 1:
    Completed 2 test(s) without failure.
...
Depth 1000:
    Completed 1001 test(s) without failure.

行が沢山出力されるので時間がかかるかと思いますが，実際には一瞬で終わっています． 先程までと違うところは，quickCheckのかわりにsmallCheckを使っているところでしょうか．また，そのあとに1000と云う引数を渡していますね．これはなんでしょうか？

これは，Depth，つまりデータ型の深さ・大きさです．先にも説明したように，SmallCheck は「深さ」ごとにデータを総当たり的に生成して，それらを全部チェックする，と云う戦略をとっています．深さが何を指すのはデータ型によって異なりますが，整数型の場合は特に最大値だと思えばよいです．smallCheck函数は深さ0から徐々に指定された深さまで増加させていって，包括的に調べる，と云う函数です．特定の深さだけを調べたい場合はdepthCheck函数が使えます．

なので，上のテストでは最大1000までの整数しかチェックできていなくて，ちょっと非効率的です．そこで，深さを最大値ではなくビット長とするように書き換えてみましょう．

data Bit = I | O deriving (Show, Read, Eq)

bitToDigit :: Bit -> Char
bitToDigit I = '1'
bitToDigit O = '0'

instance Serial Bit where
  series = cons0 O \/ cons0 I
  coseries rs d = [ \m -> case m of
                            O -> a
                            I -> b
                  | a <- alts0 rs d
                  , b <- alts0 rs d
                  ]

readBits :: Integral a => String -> a
readBits binary =
  maybe 0 fst $$ listToMaybe $$ readInt 2 (\c -> c == '0' || c == '1') digitToInt binary

test_automaton3 :: Int -> Automaton Int Char -> [Bit] -> Bool
test_automaton3 q a =
    \bits -> 
      let binary = map bitToDigit bits
          r      = readBin binary
      in if r `mod` q == 0
         then isAccepted a binary
         else not $$ isAccepted a binary

BitがBitを表わすデータ型で，その列を生成するように変更していますね．Bitを深さごとにexhaustiveに生成するために，Serial型クラスのインスタンスにしています．型からは一見なにをすればいいのかわかりづらいですが，()やMaybe aに対するインスタンス宣言を参考にしつつ，ヘルパ函数を使えば簡単にインスタンスが書けます．series函数は指定の深さのデータを生成する函数で，coseriesは，Bitを含むような別のデータ構造を生成するときに使われます．

test_automaton3では，生成した2進表現を喰わせて，それが6進数であるかどうかとオートマトンに受理されるかどうかが同値であることを確かめているだけですね．

では，確かめてみましょう．

ghci> smallCheck 16 $$ test_automaton3 6 aDivBy6'
Depth 0:
  Completed 1 test(s) without failure.
Depth 1:
  Completed 3 test(s) without failure.
...
Depth 15:
  Completed 65535 test(s) without failure.
Depth 16:
  Completed 131071 test(s) without failure.

なんかかなり時間がかかりました．実行してみるとわかりますが，15を越えたあたりから急に遅くなりはじめます．指数爆発だ……． 実際のところどれくらい時間がかかるのか，ちょっと:set +sして測ってみましょう．

ghci> depthCheck 15 $$ test_automaton3 6 aDivBy6'
Depth 15:
  Completed 65535 test(s) without failure.
(3.06 secs, 1224982104 bytes)

ghci> depthCheck 16 $$ test_automaton3 6 aDivBy6'
Depth 16:
  Completed 131071 test(s) without failure.
(6.45 secs, 2585880856 bytes)

ghci> depthCheck 17 $$ test_automaton3 6 aDivBy6'
Depth 17:
  Completed 262143 test(s) without failure.
(13.57 secs, 5465946920 bytes)

うへえ，これはひどい，メモリもかなりくってます．何とか枝刈りをしたいところです．

ここでは，n-bit長の数値を生成しているわけですが，実際には頭に0が沢山ついてるような子，例えば

000101010
010100101

みたいなのも生成しちゃってます．もちろん，こういった入力が来ても大丈夫なチェックにもなっているわけですが，ぶっちゃけ邪魔です． そこで，先頭が 1 であるものだけを判定するようにしてみましょう．

test_automaton4 :: Int -> Automaton Int Char -> [Bit] -> Property
test_automaton4 q a =
    \bits -> 
      let binary = map bitToDigit bits
          r      = maybe 0 fst $$ listToMaybe $$ readInt 2 (\c -> c == '0' || c == '1') digitToInt binary
      in (not $$ null bits) && head bits == I ==>
         if r `mod` q == 0
         then isAccepted a binary
         else not $$ isAccepted a binary

実行してみます．

Depth 15:
  Completed 65535 test(s) without failure.
  But 32768 did not meet ==> condition.
(1.71 secs, 659780920 bytes)

ghci> depthCheck 16 $$ test_automaton4 6 aDivBy6'
Depth 16:
  Completed 131071 test(s) without failure.
  But 65536 did not meet ==> condition.
(3.56 secs, 1386670368 bytes)

ghci> depthCheck 17 $$ test_automaton4 6 aDivBy6'
Depth 17:
  Completed 262143 test(s) without failure.
  But 131072 did not meet ==> condition.
(7.49 secs, 2915713216 bytes)

17bit に 7.49秒です．大分ましにはなりました．これで大体13万までは全部大丈夫，と云えます． 数学の証明にはまるでなりませんが，まあ，この値くらいまで平気であれば多分大丈夫だろう，と云うことにして，納得出来るのではないでしょうか．上限が小さすぎると云う場合は，QuickCheckの方でも乱数チェックをしているのでまあ多分大丈夫！ということで．