QuickCheck

Haskell の QuickCheck.
DFA に対する処理が妥当かどうか、という観点で論理的に満たすべき性質、を書いてみた。

最初の関数はユーティリティ。QuickCheck がデフォルトで作ってくれる、ランダムな Int の配列を、特定の DFA のアルファベットの配列に変換しランダムな文字列を生成させてテストする。もっと奇麗に書けるのかもしれない。

-- quickcheck
int2alphabet cs xs = [ cs !! mod (abs x) (length cs) | x <- xs ]
acceptInt dfa xs = accept dfa (int2alphabet (elems (alphabet dfa)) xs)

-- quick
prop_RenameSize dfa = (size dfa) == (size (rename' dfa)) -- dfa の状態名を付け替えても、状態数は変わらない
-- ある文字列が受理されるか否かは、状態名を付け替えても変わらない
prop_AcceptRename dfa xs = (acceptInt dfa xs) == (acceptInt (rename' dfa) xs) 
prop_AcceptRenameRename dfa xs = (acceptInt dfa xs) ==
                                 (acceptInt (rename' (rename' dfa)) xs)
-- ある文字列が受理されるか否かは、DFA を NFA に変換しもう一度 DFA に変換しても変わらない
prop_Conv dfa xs = (acceptInt dfa xs) == (acceptInt (convNFAToDFA (convDFAToNFA dfa)) xs)

こんな感じで使い、プログラムが正しいことを確認する。

*FA> dfa1
DFA
 States: ["q0","q1"]
q0: "q0"
fs: ["q1"]
delta: 
	"q0" 'a' => "q1"
	"q0" 'b' => "q0"
	"q1" 'a' => "q0"
	"q1" 'b' => "q1"

*FA> quickCheck (prop_AcceptRename dfa1)
+++ OK, passed 100 tests.
*FA> *FA> quickCheck (prop_Conv dfa1)
+++ OK, passed 100 tests.

なお、ランダムな文字列なので、受理される/しないが偏っている可能性があり、十分なテストになっていないかもしれない。それはまた別に考える。