[Haskell-cafe] ANN: LeanCheck v0.9.0 -- enumerative property testing
Johannes Waldmann
johannes.waldmann at htwk-leipzig.de
Thu Jan 17 17:28:32 UTC 2019
Yes, leancheck is awesome.
> When should I reach to enumerative testing?
I think enumerative testing
is best suited to algebraic data types.
https://mail.haskell.org/pipermail/haskell-cafe/2018-September/129951.html
In the past I had one standard example
where random enumeration seems better than enumerative:
(non)associativity of floating point ops
(I like to use this in teaching)
That's immediate in Quickcheck
quickCheck $ \ x y z -> (x::Double) + (y+z) == (x+y)+z
*** Failed! Falsifiable (after 3 tests and 3 shrinks):
-0.3
-1.4266097805446862
-1.2543117889178947
You don't get to see a counterexample in Smallcheck
Prelude Test.SmallCheck> smallCheck 5 $ \ x y z -> (x::Double) + (y+z)
== (x+y)+z
Completed 50653 tests without failure.
To my surprise, we now have
Prelude Test.LeanCheck> check $ \ x y z -> (x::Double) + (y+z) == (x+y)+z
*** Failed! Falsifiable (after 87 tests):
0.0 Infinity (-Infinity)
and I get the above (with "real" numbers) via
Prelude Test.LeanCheck> checkFor 1000 $ \ x y z -> isInfinite x ||
isInfinite y || isInfinite z || (x::Double) + (y+z) == (x+y)+z
*** Failed! Falsifiable (after 306 tests):
1.0 1.0 0.3333333333333333
Turns out the enumeration in Leancheck uses Rationals,
while Smallcheck uses encodeFloat, which happens to
produce only "nice" numbers (very few bits set) in the beginning.
Prelude Test.LeanCheck> list 3 series :: [Double]
[0.0,1.0,-1.0,2.0,0.5,-2.0,4.0,0.25,-0.5,-4.0,-0.25]
Prelude Test.LeanCheck> take 12 $ list :: [Double]
[0.0,1.0,-1.0,Infinity,0.5,2.0,-Infinity,-0.5,-2.0,0.3333333333333333,3.0,-0.3333333333333333]
- J.W.
PS: this post wouldn't be complete without me complaining
that I cannot (easily) put the type annotation
where it belongs - in the declaration of the name:
Prelude Test.LeanCheck> check $ \ (x::Double) y z -> x + (y+z) == (x+y)+z
<interactive>:22:12: error:
Illegal type signature: ‘Double’
Type signatures are only allowed in patterns with ScopedTypeVariables
Wat? TypeVariables? There aren't any!
More information about the Haskell-Cafe
mailing list