FOP/ex8.4 - 大久保弘崇

ex8.8

Lava Tutorialの類似した演習問題4.8によると、
証明器の呼び出し関数がIOモナドであることを利用して、単に順番に呼び出せということらしい。

verifyFor prover prop ns = sequence [ prover (prop n) | n <- ns ]
ex88 = verifyFor satzoo  prop_AdderCommutative_ForSize [1..32]
 

ex8.9

adder2ではなくadderと同じインタフェースのsubtractorを検証せよという問題文の意図が、
どこまで厳密に確認しろと言っているのかよくわからないところが困る。
長さが等しくない場合も含めて、ではありえない面倒臭さになるので、
桁下がりの初期値なども無視して、正常系のテストのみ。
加算をHaskellの(+)でなくadderで行っている点が怪しいので△

ex89 :: Int -> Property
ex89 n =
  forAll (list n) $ ¥ as ->
    forAll (list n) $ ¥ bs ->
      prop_SubtractorCorrect (as, bs)
prop_SubtractorCorrect :: ([Bit],[Bit]) -> Bit
prop_SubtractorCorrect (as, bs) = ok where
  (cs, co) = adder (low, (as, bs))
  (es, eo) = subber (low, (cs, as))
  ok = eo <=> co <&> bs <==> es
 

コメント