競技プログラミングでは、提出したプログラムが誤答（WA）だった場合に「どのような入力について」答えを間違えたのか（参加者には）分からないことが多いです。
こういう場合はエスパーするなり眼力でソースコードをぐっと睨んだりするとバグが発見できる場合もありますが、初心者にはそういうのは難しいでしょう。
この記事では、HaskellのQuickCheckというライブラリーを使って、「ランダムにテストケースを生成して素朴な解と一致するか」を自動で検証させます。QuickCheckはテストに失敗した場合に「どういう入力例に対して失敗したか」も教えてくれるので、デバッグにも役立ちます。
この記事は筆者が先日YouTubeに上げた動画を文章で書き直したものです。動画で触れられなかった・触れるのを忘れていた補足説明みたいなものも若干含んでいます。この記事と動画、両方見ていただけると嬉しいです。
今回取り上げる問題は、AtCoder Beginner Contest 175のC問題です。
素朴な解
入出力の部分は適当に用意します。
import Data.Char (isSpace)
import Data.Int (Int64)
import Data.List (unfoldr)
naive :: Integer -> Integer -> Integer -> Integer
naive x k d = undefined
main = do
[x,k,d] <- map fromInteger . unfoldr (BS.readInteger . BS.dropWhile isSpace) <$> BS.getLine
print $ naive x k dまずは素朴な解（愚直解）を実装します。素朴な解では、k回移動した後にありうるすべての位置を計算し、その中で原点との距離が最小のものを選びます。
ここでは、リストモナドによる非決定的計算を使ってみましょう。位置 t から1回の移動を行った後に高橋くんがいる座標は t – d または t + d です。その計算を oneStep 関数として、それをk回適用したものが、k回後にいる可能性のある場所です。あとはそれの絶対値の最小値を取れば良いです。コードとしては次のようになります：
naive :: Integer -> Integer -> Integer -> Integer
naive x k d = minimum $ map abs $ do
-- oneStepをk回適用した結果を返す
let loop 0 t = return t
loop i t = do
u <- oneStep t
loop (i - 1) u
loop k x
where
-- 1回の移動後にいる座標を返す
oneStep :: Integer -> [Integer]
oneStep t = [t - d, t + d]「関数をk回適用する」という部分には iterate 関数を使うという手もあります。「xに関数fをk回適用する」基本系は iterate f x !! k ですが、今回適用したい関数はモナディックな計算なので、少し変えて
naive x k d = minimum $ map abs $ iterate (>>= oneStep) (pure x) !! fromInteger k
where ...とします。
あるいは、リストモナドのモナドっぽい書き方をやめて concatMap で
naive x k d = minimum $ map abs $ iterate (concatMap oneStep) (pure x) !! fromInteger k
where ...と書くこともできます。
いずれも素朴な解法で、\(2^k\)通りの全てを検証するので指数時間かかります。提出すると当然TLEです。
本命の解
続いて、本命の解を実装します。なんとなく「xをdで割るんだろうな」という感じがします。kが十分に大きければ、xをdで割ったあまりをrとすると「最終的な位置」は r か r - d になりそうです。kがそこまで大きくなければ、「ずっと原点方向に移動する」のがベストになりそうです。また、原点に関して諸々を反転させても答えは変わらないので、xは絶対値を取って計算しても構いません。適当に書いてみましょう。
solve :: Int64 -> Int64 -> Int64 -> Int64
solve x k d = let (q,r) = abs x `quotRem` d
in if q <= k then
min r (abs (r - d))
else
x - k * dこのコードはいろいろバグっているので提出するまでもなくWAなのですが、一応提出してみた結果がこちらです。
ここからが本題の、「本命の解のデバッグ」です。
本命の解のデバッグ
問題にはいくつか入力例が付属しますが、この「本命だがバグった解」は入力例1から3をパスします。入力例4は間違えるのでそれで一つバグを潰せますが、ここでは与えられた入力例に頼らずにデバッグしてみましょう。
方針としては、「ランダムな入力を生成し、素朴な解と本命の解の出力が一致することを確かめる」となります。テストのために「ランダムな入力を生成する」のは自分でやると結構面倒ですが、Haskellの場合はQuickCheckというライブラリーを使うと、ランダムな入力を使ったテストを比較的簡単に実行できます。
QuickCheckは外部のパッケージなので、利用するには設定が必要です。プロジェクトの.cabalやpackage.yamlに書くか、プロジェクトを作っていない場合は stack repl --package bytestring --package QuickCheck という風にしましょう。
QuickCheckでは「ある性質が成り立つか」をランダムな入力でテストします。ここで確かめたい性質は「素朴な解と本命の解の出力が一致する」ことです。なので、そういう風に条件を（関数として）記述します。
-- 確かめたい条件
prop :: Int64 -> Int64 -> Int64 -> Bool
prop x k d = toInteger (solve x k d) == naive (toInteger x) (toInteger k) (toInteger d)この条件を Test.QuickCheck モジュールの quickCheck 関数に渡してやると、テストが行われます。ここではREPLから呼び出してみますが、ファイルの中に runTest = quickCheck prop というような補助関数を書いてやっても良いでしょう。
*Main> Test.QuickCheck.quickCheck prop
*** Failed! Exception: 'divide by zero' (after 1 test and 4 shrinks):
0
0
0ゼロ除算が発生しました。QuickCheckが d = 0 という範囲外の入力を生成してしまったようです。
（ランダムに入力を生成しているのに提示された例が x = k = d = 0 という「綺麗な」値なのは不思議だ！と思われるかもしれません。実はQuickCheckは反例を見つけた時に「なるべく小さい」反例を探索してそれを提示するようになっています。なので、x = k = d = 0 が提示されるのはある意味で必然なのです。この「小さい反例を探索する」ことをQuickCheckでは shrink （縮小）と呼んでいます。）
QuickCheckは、デフォルトでは型に基づいて入力を生成します。しかし、関数が想定する入力というのは型のとりうる値すべてとは限りません。そういう場合の対処法はいくつかあります。
==> 演算子による入力範囲の指定
ここでは、QuickCheckの提供する ==> 演算子を使った解決方法を見てみます。==> は数学の「ならば」記号みたいな感じで、左辺の前提条件が満たされた場合のみに右辺の条件を実行します。左辺の条件が満たされない場合はその入力に対するテストは行われません。
（入力の範囲を指定するのに ==> 演算子を使うのは本当は望ましくありません。望ましくない理由およびより良い方法は後ろの方で解説します。）
==> 演算子の型は
(==>) :: Testable prop => Bool -> prop -> Propertyで、Test.QuickCheck モジュールの Property 型を返します。 Property 型というのはテストの成否だけではなく、「どのような入力についてテストが行われたか」というような追加の情報も持っています。
まずは、「入力の d が 0 ではない」という条件を課してみましょう。
import qualified Test.QuickCheck as QC
prop :: Int64 -> Int64 -> Int64 -> QC.Property
prop x k d = d /= 0 QC.==> toInteger (solve x k d) == naive (toInteger x) (toInteger k) (toInteger d)改めてテストしてみると、
*Main> Test.QuickCheck.quickCheck prop
*** Failed! Falsified (after 4 tests and 2 shrinks):
2
0
3という失敗例が出ました。今度はkが0の時に失敗したようです。
問題文によると k は1以上ですから、そのように条件を書き換えましょう。よく考えると d も1以上なので、 d の条件もそうしましょう。
prop :: Int64 -> Int64 -> Int64 -> QC.Property
prop x k d = k >= 1 && d >= 1 QC.==> toInteger (solve x k d) == naive (toInteger x) (toInteger k) (toInteger d)そうすると、今度は真面目な（範囲外の入力ではない）失敗例が出てきました。
*Main> Test.QuickCheck.quickCheck prop
*** Failed! Falsified (after 2 tests):
0
1
1失敗例を元にデバッグする際は、「失敗例を与える入力」だけではなく、「条件式の両辺がどういう値だったのか」というのもわかると便利です。そのためには、等価性の比較に使っている == 演算子を、QuickCheckの === 演算子（否定は =/=）に置き換えてやれば良いです。=== 演算子は「両辺がどういう値だったせいで不一致と判断されたのか」という追加の情報を持つので、 Bool ではなく Property 型を返します。
prop :: Int64 -> Int64 -> Int64 -> QC.Property
prop x k d = k >= 1 && d >= 1 QC.==> toInteger (solve x k d) QC.=== naive (toInteger x) (toInteger k) (toInteger d)すると、実行結果が
*Main> Test.QuickCheck.quickCheck prop
*** Failed! Falsified (after 1 test):
0
1
1
0 /= 1となります。左辺（本命だがバグった解）は 0、右辺（素朴な解）は 1 を返したようです。
これはアレです、 min で r と (abs (r - d)) を比較しているのがおかしいのです。本当は k - q の偶奇で判断すべきです。
solve :: Int64 -> Int64 -> Int64 -> Int64
solve x k d = let (q,r) = abs x `quotRem` d
in if q <= k then
-- 修正後
if even (k - q) then
r
else
abs (r - d)
else
x - k * dタイムアウトと、ジェネレーターによる入力範囲の指定
今度は、テストが終了しなくなってしまいました。入力が大きすぎて、素朴な解の実行に時間がかかりすぎていると思われます。
時間のかかりすぎるテストの実行時間を制限するには、 within 関数が利用できます。引数はマイクロ秒単位で指定します。ここでは、実行時間を100ミリ秒に制限してみましょう。
prop :: Int64 -> Int64 -> Int64 -> QC.Property
prop x k d = QC.within (100 * 1000) $ k >= 1 && d >= 1 QC.==> toInteger (solve x k d) QC.=== naive (toInteger x) (toInteger k) (toInteger d)実行してみると、「タイムアウトする例」が表示されます。（先程のコードはまだバグっているので、確率によっては普通のバグに対する反例が出てくるかもしれません。）
*Main> Test.QuickCheck.quickCheck prop
*** Failed! Timeout (after 8 tests and 6 shrinks):
0
16
3k が 16 ぐらいになると素朴な解の実行に時間がかかりすぎるようです。k は「1以上15以下」で生成したいところです。
QuickCheckで入力の生成方法を具体的に指定するには、Gen 型と forAll 系の関数を使います。forAll 関数は第1引数に Gen 型のジェネレーターを指定し、第2引数に条件（生成される値を受け取る関数）を指定します。
指定された範囲の値を生成するには choose 関数を使います。
module Test.QuickCheck where
data Gen a
choose :: Random a => (a, a) -> Gen a
forAll :: (Show a, Testable prop) => Gen a -> (a -> prop) -> Property使用例は次のようになります。
prop :: Int64 -> Int64 -> QC.Property
prop x d = QC.forAll (QC.choose (1, 15)) $ \k -> d >= 1 QC.==> toInteger (solve x k d) QC.=== naive (toInteger x) (toInteger k) (toInteger d)この状態でテストしてみると、
*Main> Test.QuickCheck.quickCheck prop
*** Failed! Falsified (after 17 tests and 9 shrinks):
-5
1
4
-9 /= 1というような「まともな」反例が出てきました。これをデバッグすると、 solve 関数の最後の行で x に abs をつけ忘れていることがわかります。これを修正すると、
*Main> Test.QuickCheck.quickCheck prop
+++ OK, passed 100 tests; 117 discarded.という風に、テストがパスします。お疲れ様でした。
==> の問題点と、出来合いの型による入力範囲の指定
テスト結果をみると、「passed 100 tests」の他に「117 discarded」と出力されています。これは「100回の「成功」を得るまでに217個の入力を生成して、うち117個は ==> の前提条件を満たさないので捨てたよ」という意味です。
この場合は結局テストがパスしているので良いのですが、もっと大規模なテストで ==> を使いまくると「いくらテストケースを生成しても ==> の前提条件を満たすものが少なすぎるから、十分な数の「成功」を得るのを諦めてしまったよ😢」という事態が発生してしまいます。
前提条件が複雑なら ==> の使用は仕方がありませんが、そうでない場合はなるべくテストケースのジェネレーターをカスタマイズする方向性で考えるべきです。
テストケースのジェネレーターのカスタマイズには、先述した Gen 型と forAll 関数を使う方法がありますが、ここではもっとお手軽な方法を紹介します。
QuickCheckは、カスタマイズされたジェネレーターを持つnewtype wrapperをいくつか提供しています。例えば「0でない Int 型の値が欲しい」という場合には
prop :: NonZero Int -> ...
prop (NonZero x) ... = ...という風に NonZero 型を使えばOKです。
今回は d として「1以上の値」が欲しいので、 Positive 型を使って
prop :: Int64 -> QC.Positive Int64 -> QC.Property
prop x (QC.Positive d) = QC.forAll (QC.choose (1, 15)) $ \k -> toInteger (solve x k d) QC.=== naive (toInteger x) (toInteger k) (toInteger d)とします。これでテストを実行すると
*Main> Test.QuickCheck.quickCheck prop
+++ OK, passed 100 tests.と、 discard される入力がなくなりました。
AtCoderへの提出について
2020年8月現在のAtCoderのHaskell環境には、QuickCheckが含まれています。なので、 import Test.QuickCheck を含むコードをそのままAtCoderに提出することができます。ただし、バージョンがQuickCheck-2.13.2と若干古くなっているので注意してください。
他の利用例
QuickCheckは「本命の解と素朴な解が一致する」ことの他に、例えば「REになる原因を調査する」ことにも使えます。
REの原因は、入力の解釈のミス、リストや配列の範囲外アクセス、ゼロ除算、空リストに対するheadやmaximumなどが典型的ですが、ヒントがない状態でデバッグするのは大変です。普通に性質のテストを書いても実行時エラーは補足できます（この記事でもゼロ除算が発生していました）が「関数がエラーを投げずに終了する」ことだけをテストする場合は total 関数が使えます。
まとめ
この記事ではABC175-Cを題材に、
- QuickCheckの基本的な使い方
==>演算子による前提条件の記述Gen型とforAll関数によるジェネレーターの指定（入力範囲の指定）- QuickCheckの提供するnewtype wrapperによる簡易的なジェネレーターの指定
をざっくりと解説しました。
QuickCheckは使いこなすと強力なツールです。頑張りましょう。
