diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -3,6 +3,8 @@ [![Extrapolate Build Status][build-status]][build-log] [![Extrapolate on Hackage][hackage-version]][extrapolate-on-hackage] +[![Extrapolate on Stackage LTS][stackage-lts-badge]][extrapolate-on-stackage-lts] +[![Extrapolate on Stackage Nightly][stackage-nightly-badge]][extrapolate-on-stackage-nightly] Extrapolate is a [property-based testing] library for [Haskell] capable of reporting generalized counter-examples. @@ -118,6 +120,12 @@ For type signatures, other options and uses, see [Extrapolate's API documentation]. +There are two other tools for [Haskell] capable of producing generalized +counter-examples: [SmartCheck] and [Lazy SmallCheck 2012]. + +Extrapolate was accepted for presentation at [IFL 2017], a link to a +pre-symposium proceedings draft paper will be listed here soon. + [extrapolate-on-hackage]: https://hackage.haskell.org/package/extrapolate [Extrapolate from Hackage]: https://hackage.haskell.org/package/extrapolate [Extrapolate's API documentation]: https://hackage.haskell.org/package/extrapolate/docs/Test-Extrapolate.html @@ -132,6 +140,15 @@ [cabal]: https://www.haskell.org/cabal/ [property-based testing]: https://github.com/rudymatela/leancheck/blob/master/doc/tutorial.md +[IFL 2017]: http://iflconference.org/ +[SmartCheck]: https://github.com/leepike/SmartCheck +[Lazy SmallCheck 2012]: https://github.com/UoYCS-plasma/lazysmallcheck2012 + [build-status]: https://travis-ci.org/rudymatela/extrapolate.svg?branch=master [build-log]: https://travis-ci.org/rudymatela/extrapolate [hackage-version]: https://img.shields.io/hackage/v/extrapolate.svg +[stackage-lts-badge]: http://stackage.org/package/extrapolate/badge/lts +[stackage-nightly-badge]: http://stackage.org/package/extrapolate/badge/nightly +[extrapolate-on-stackage]: http://stackage.org/package/extrapolate +[extrapolate-on-stackage-lts]: http://stackage.org/lts/package/extrapolate +[extrapolate-on-stackage-nightly]: http://stackage.org/nightly/package/extrapolate diff --git a/TODO.md b/TODO.md --- a/TODO.md +++ b/TODO.md @@ -4,37 +4,9 @@ A non-exhaustive list of things TO DO for Extrapolate. -cleanup -------- - -* `renames1`: - rename show functions: - - move `showCE` to `Core`; - - add and use `Core.showCCE`; - - rename `IO.showCEC` to `IO.showCEandGens`; - -* `renames2`: - rename counterexamples: - - rename `counterExamples*` to `counterExamples*E`; - - add `counterExamples* :: ... String ...`; - -* `cleanup`: - cleanup and remove unused functions, like `showCEG`; - thighten exports, removing uneeded functions (`backgroundWith`). - - examples -------- -* `add-redblack-eg`: - add the redblacktree example from Small/SmartCheck/Okasaki. - see `ideal-generalization`. - Also described on: http://matt.might.net/articles/quick-quickcheck/ - - It has been added, but cannot generalize the counter-examples found: during - generalization, the very exceptions that cause the error, make the - generalization fail. Somehow catch those errors on generalization. - * `ideal-generalizations`: Add examples of ideal generalizations as described in past paper by human experts. The counter example is `blah` because the property fails for every @@ -79,14 +51,6 @@ the above is for the last property of the list example -* `add-derive-tests`: - add tests of derivation; - -* `show-and-expr-display`: - display counterExamples both as Show and Expr, I don't know how easy is to - use show since counterExamples are represented as Exprs, I don't think I can - eval because I am not bound in a type context. - * `renaming`: possibly print `(Div (C 0) (Add (C x) (C (negate x))))` which is equivalent to `(Div (C 0) (Add (C x) (C y))) when y == negate x` @@ -134,11 +98,6 @@ * `single-then-multi`: only do vassignments *after* finding a failing single variable instance. I'll have to re-test, but the time I save may pay off. - -* `no-listable-tuples`: - there is no need to include listable tuples in the instances list (or at - least no need to use it). Instead of having `xy` we would get `(x,y)`. - However, maybe it is fine as it is. won't fix --------- diff --git a/extrapolate.cabal b/extrapolate.cabal --- a/extrapolate.cabal +++ b/extrapolate.cabal @@ -1,11 +1,11 @@ name: extrapolate -version: 0.2.1 +version: 0.2.2 synopsis: generalize counter-examples of test properties description: Extrapolate is a tool able to provide generalized counter-examples of test properties where irrelevant sub-expressions are replaces with variables. . - For the incorrect property @\xs -> nub xs == (xs::[Int])@: + For the incorrect property @\\xs -> nub xs == (xs::[Int])@: . * @[0,0]@ is a counter-example; . @@ -31,7 +31,7 @@ source-repository this type: git location: https://github.com/rudymatela/speculate - tag: v0.2.1 + tag: v0.2.2 library exposed-modules: Test.Extrapolate @@ -41,12 +41,12 @@ , Test.Extrapolate.Exprs , Test.Extrapolate.IO , Test.Extrapolate.TypeBinding - other-modules: Test.Extrapolate.Utils + , Test.Extrapolate.Utils other-extensions: TemplateHaskell, CPP build-depends: base >= 4 && < 5 - , leancheck >= 0.6.4 + , leancheck >= 0.6.5 , template-haskell - , speculate >= 0.2.6 + , speculate >= 0.2.8 hs-source-dirs: src default-language: Haskell2010 @@ -54,14 +54,22 @@ type: exitcode-stdio-1.0 main-is: test-extrapolate.hs other-modules: Test - hs-source-dirs: src, tests - build-depends: base >= 4 && < 5, leancheck, speculate, template-haskell + hs-source-dirs: tests + build-depends: base >= 4 && < 5, leancheck, speculate, extrapolate default-language: Haskell2010 test-suite derive type: exitcode-stdio-1.0 main-is: test-derive.hs other-modules: Test - hs-source-dirs: src, tests - build-depends: base >= 4 && < 5, leancheck, speculate, template-haskell + hs-source-dirs: tests + build-depends: base >= 4 && < 5, leancheck, speculate, extrapolate + default-language: Haskell2010 + +test-suite utils + type: exitcode-stdio-1.0 + main-is: test-utils.hs + other-modules: Test + hs-source-dirs: tests + build-depends: base >= 4 && < 5, leancheck, speculate, extrapolate default-language: Haskell2010 diff --git a/src/Test/Extrapolate.hs b/src/Test/Extrapolate.hs --- a/src/Test/Extrapolate.hs +++ b/src/Test/Extrapolate.hs @@ -61,7 +61,6 @@ , module Test.Extrapolate.TypeBinding , module Test.LeanCheck , module Test.LeanCheck.Utils.TypeBinding - , ordering ) where @@ -83,8 +82,3 @@ , checkResultFor ) import Test.LeanCheck.Utils.TypeBinding --- TODO: add the following function `ordering` into LeanCheck's TypeBinding --- module; release a new LeanCheck; remove it from here and bump version --- requirement. -ordering :: Ordering -ordering = undefined diff --git a/src/Test/Extrapolate/Basic.hs b/src/Test/Extrapolate/Basic.hs --- a/src/Test/Extrapolate/Basic.hs +++ b/src/Test/Extrapolate/Basic.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} -- for GHC <= 7.8 -- | -- Module : Test.Extrapolate.Basic -- Copyright : (c) 2017 Rudy Matela @@ -23,3 +24,61 @@ instances q = this q id -- The following would allow zero denominators -- expr (n % d) = constant "%" ((%) -:> n) :$ expr n :$ expr d + +instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d + , Generalizable e ) + => Generalizable (a,b,c,d,e) where + name xyzwv = name x ++ name y ++ name z ++ name w ++ name v + where (x,y,z,w,v) = xyzwv + expr (x,y,z,w,v) = constant ",,,," ((,,,,) ->>>>>: (x,y,z,w,v)) + :$ expr x :$ expr y :$ expr z :$ expr w :$ expr v + instances xyzwv = this xyzwv $ instances x . instances y . instances z + . instances w . instances v + where (x,y,z,w,v) = xyzwv + +instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d + , Generalizable e, Generalizable f ) + => Generalizable (a,b,c,d,e,f) where + name xyzwvu = name x ++ name y ++ name z ++ name w ++ name v ++ name u + where (x,y,z,w,v,u) = xyzwvu + expr (x,y,z,w,v,u) = constant ",,,,," ((,,,,,) ->>>>>>: (x,y,z,w,v,u)) + :$ expr x :$ expr y :$ expr z :$ expr w :$ expr v :$ expr u + instances xyzwvu = this xyzwvu $ instances x . instances y . instances z + . instances w . instances v . instances u + where (x,y,z,w,v,u) = xyzwvu + +instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d + , Generalizable e, Generalizable f, Generalizable g ) + => Generalizable (a,b,c,d,e,f,g) where + name xyzwvut = name x ++ name y ++ name z ++ name w + ++ name v ++ name u ++ name t + where (x,y,z,w,v,u,t) = xyzwvut + expr (x,y,z,w,v,u,t) = constant ",,,,,," ((,,,,,,) ->>>>>>>: (x,y,z,w,v,u,t)) + :$ expr x :$ expr y :$ expr z :$ expr w + :$ expr v :$ expr u :$ expr t + instances xyzwvut = this xyzwvut + $ instances x . instances y . instances z . instances w + . instances v . instances u . instances t + where (x,y,z,w,v,u,t) = xyzwvut + +#if __GLASGOW_HASKELL__ < 710 +-- No 8-tuples for you: +-- On GHC 7.8, 8-tuples are not Typeable instances. We could add a standalone +-- deriving clause, but that may cause trouble if some other library does the +-- same. User should declare Generalizable 8-tuples manually when using GHC <= +-- 7.8. +#else +instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d + , Generalizable e, Generalizable f, Generalizable g, Generalizable h ) + => Generalizable (a,b,c,d,e,f,g,h) where + name xyzwvuts = name x ++ name y ++ name z ++ name w + ++ name v ++ name u ++ name t ++ name s + where (x,y,z,w,v,u,t,s) = xyzwvuts + expr (x,y,z,w,v,u,t,s) = constant ",,,,,,," ((,,,,,,,) ->>>>>>>>: (x,y,z,w,v,u,t,s)) + :$ expr x :$ expr y :$ expr z :$ expr w + :$ expr v :$ expr u :$ expr t :$ expr s + instances xyzwvuts = this xyzwvuts + $ instances x . instances y . instances z . instances w + . instances v . instances u . instances t . instances s + where (x,y,z,w,v,u,t,s) = xyzwvuts +#endif diff --git a/src/Test/Extrapolate/Core.hs b/src/Test/Extrapolate/Core.hs --- a/src/Test/Extrapolate/Core.hs +++ b/src/Test/Extrapolate/Core.hs @@ -34,10 +34,14 @@ , counterExampleGen , counterExampleGens + , generalizations , generalizationsCE , generalizationsCEC , generalizationsCounts + , weakestCondition + , candidateConditions + , conditionalGeneralization , matchList , newMatches @@ -168,20 +172,27 @@ instances xy = this xy $ instances (fst xy) . instances (snd xy) -instance (Generalizable a, Generalizable b, Generalizable c) => Generalizable (a,b,c) where - name xyz = name ((\(x,_,_) -> x) xyz) - ++ name ((\(_,y,_) -> y) xyz) - ++ name ((\(_,_,z) -> z) xyz) +instance (Generalizable a, Generalizable b, Generalizable c) + => Generalizable (a,b,c) where + name xyz = name x ++ name y ++ name z + where (x,y,z) = xyz expr (x,y,z) = constant ",," ((,,) ->>>: (x,y,z)) :$ expr x :$ expr y :$ expr z - instances xyz = this xyz $ instances (fst xyz) - . instances (snd xyz) - . instances (trd xyz) - where - fst (x,_,_) = x - snd (_,y,_) = y - trd (_,_,z) = z + instances xyz = this xyz $ instances x . instances y . instances z + where (x,y,z) = xyz +instance (Generalizable a, Generalizable b, Generalizable c, Generalizable d) + => Generalizable (a,b,c,d) where + name xyzw = name x ++ name y ++ name z ++ name w + where (x,y,z,w) = xyzw + expr (x,y,z,w) = constant ",,," ((,,,) ->>>>: (x,y,z,w)) + :$ expr x :$ expr y :$ expr z :$ expr w + instances xyzw = this xyzw $ instances x + . instances y + . instances z + . instances w + where (x,y,z,w) = xyzw + instance Generalizable a => Generalizable [a] where name xs = name (head xs) ++ "s" expr (xs@[]) = showConstant ([] -: xs) @@ -428,22 +439,34 @@ weakestCondition :: Testable a => Int -> a -> [Expr] -> Expr weakestCondition m p es = head $ + [ c | c <- candidateConditions p es + , isCounterExampleUnder m p c es + ] ++ [expr False] + where + +candidateConditions :: Testable a => a -> [Expr] -> [Expr] +candidateConditions p es = expr True : [ c - | c <- constant "True" True : candidates + | c <- candidateExpressions p es , typ c == boolTy + , hasVar c , not (isAssignment c) - , not (isAssignmentTest is m c) - , isCounterExampleUnder m p c es - ] ++ [ constant "False" False ] + , not (isAssignmentTest is (maxTests p) c) + ] where is = tinstances p - candidates = concat . take (maxConditionSize p) . expressionsTT - . foldr (\/) [vs ++ esU] - $ [ eval (error msg :: [[Expr]]) ess - | Instance "Listable" _ [ess] <- tinstances p ] + +-- | Canditate expressions to appear in conditions +candidateExpressions :: Testable a => a -> [Expr] -> [Expr] +candidateExpressions p es = concat . take (maxConditionSize p) . expressionsTT + . foldr (\/) [vs ++ esU] + $ [ eval (error msg :: [[Expr]]) ess + | Instance "Listable" _ [ess] <- is ] + where vs = [Var n t | (t,n) <- vars es] - esU = concat [es | Instance "Background" _ es <- tinstances p] - msg = "weakestCondition: wrong type, not [[Expr]]" + esU = concat [es | Instance "Background" _ es <- is] + msg = "canditateConditions: wrong type, not [[Expr]]" + is = tinstances p isCounterExampleUnder :: Testable a => Int -> a -> Expr -> [Expr] -> Bool isCounterExampleUnder m p c es = and' diff --git a/src/Test/Extrapolate/TypeBinding.hs b/src/Test/Extrapolate/TypeBinding.hs --- a/src/Test/Extrapolate/TypeBinding.hs +++ b/src/Test/Extrapolate/TypeBinding.hs @@ -10,24 +10,7 @@ -- Some type binding operators that are useful when defining Generalizable -- instances. module Test.Extrapolate.TypeBinding - ( argTypes0 - , argTypes1 - , argTypes2 - , argTypes3 - , argTypes4 - , argTypes5 - , argTypes6 - , argTypes7 - , argTypes8 - , argTypes9 - , argTypes10 - , argTypes11 - , argTypes12 - - , argTys1 - , argTys2 - - , argTy1of1 + ( argTy1of1 , argTy1of2, argTy2of2 , argTy1of3, argTy2of3, argTy3of3 , argTy1of4, argTy2of4, argTy3of4, argTy4of4 @@ -38,8 +21,6 @@ -- TODO: reexport LeanCheck's typebinding operators --- TODO: remove argTypesN and argTysN, unused and uneeded - argTypes0 :: a -> a argTypes0 f = f @@ -100,13 +81,6 @@ -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) argTypes12 f _ _ _ _ _ _ _ _ _ _ _ _ = f - - -argTys1 :: con a -> a -> con a -argTys1 x _ = x - -argTys2 :: con a b -> a -> b -> con a b -argTys2 x _ _ = x argTy1of1 :: con a -> a diff --git a/src/Test/Extrapolate/Utils.hs b/src/Test/Extrapolate/Utils.hs --- a/src/Test/Extrapolate/Utils.hs +++ b/src/Test/Extrapolate/Utils.hs @@ -7,7 +7,11 @@ -- This module is part of Extrapolate, -- a library for generalization of counter-examples. -- --- Misc. utilities. +-- Miscellaneous utility functions. +-- +-- This is not intended to be used by users of Extrapolate, only by modules of +-- Extrapolate itself. Expect symbols exported here to come and go with every +-- minor version. module Test.Extrapolate.Utils ( (+++) , nubMerge diff --git a/tests/Test.hs b/tests/Test.hs --- a/tests/Test.hs +++ b/tests/Test.hs @@ -12,16 +12,26 @@ , (-:-), ll, llb + , _i, xx, yy + , _is, xxs, yys , zero, one , false, true + , elem' + , nothing, nothingBool, just , comma + , (-==-) + , (-/=-) + , (-<-) + , (-<=-) + -- * Properties and Tests , generalizableOK + , exprOK , idExprEval, showOK , instancesOK , namesOK, sameNamesIn, namesIn @@ -40,6 +50,7 @@ import Test.Speculate.Expr.Instance as I import Data.Typeable (typeOf) import Data.List (isPrefixOf, sort) +import Data.Maybe (fromMaybe) import Test.Extrapolate import Test.Extrapolate.Core hiding (false, true) @@ -82,6 +93,16 @@ ll :: Expr ll = expr ([] :: [Int]) +_i, xx, yy :: Expr +_i = var "" int +xx = var "x" int +yy = var "y" int + +_is, xxs, yys :: Expr +_is = var "" [int] +xxs = var "xs" [int] +yys = var "ys" [int] + zero :: Expr zero = expr (0 :: Int) @@ -103,6 +124,11 @@ nothingBool :: Expr nothingBool = constant "Nothing" (Nothing :: Maybe Bool) +elem' :: Expr -> Expr -> Expr +elem' x xs = elemE :$ x :$ xs + where + elemE = constant "elem" (elem :: Int -> [Int] -> Bool) + just :: Expr -> Expr just x = justE :$ x where @@ -127,12 +153,38 @@ commaEbi = constant "," ((,) ->>: (bool,int)) commaEbb = constant "," ((,) ->>: (bool,bool)) +(-==-) :: Expr -> Expr -> Expr +e1 -==- e2 = + fromMaybe (error $ "(-==-): cannot equate " ++ show e1 ++ " and " ++ show e2) + (equation preludeInstances e1 e2) +infix 4 -==- +(-/=-) :: Expr -> Expr -> Expr +e1 -/=- e2 = constant "/=" ((/=) :: Int -> Int -> Bool) :$ e1 :$ e2 +infix 4 -/=- +-- TODO: improve above after changing Speculate + +(-<=-) :: Expr -> Expr -> Expr +e1 -<=- e2 = + fromMaybe (error $ "(-<=-): cannot lessEq " ++ show e1 ++ " and " ++ show e2) + (comparisonLE preludeInstances e1 e2) +infix 4 -<=- + +(-<-) :: Expr -> Expr -> Expr +e1 -<- e2 = + fromMaybe (error $ "(-<-): cannot less " ++ show e1 ++ " and " ++ show e2) + (comparisonLT preludeInstances e1 e2) +infix 4 -<- + + + -- Properties and tests -- generalizableOK :: (Eq a, Show a, Generalizable a) => Int -> a -> Bool generalizableOK n x = holds n (exprOK -:> x) - && instancesOK x + && instancesOK (und -: x) + where + und = error "generalizableOK: this should not get evaluated" exprOK :: (Eq a, Show a, Generalizable a) => a -> Bool exprOK = idExprEval &&& showOK diff --git a/tests/test-extrapolate.hs b/tests/test-extrapolate.hs --- a/tests/test-extrapolate.hs +++ b/tests/test-extrapolate.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} -- Copyright (c) 2017 Rudy Matela. -- Distributed under the 3-Clause BSD licence (see the file LICENSE). import Test @@ -60,17 +61,20 @@ , generalizableOK n (int,bool) , generalizableOK n ((),integer) , generalizableOK n ((),bool,integer) --- TODO: implement further tuple instances (4,5,6) and uncomment below ---, generalizableOK n (int,(),bool,integer) ---, generalizableOK n (int,(),bool,integer,char) ---, generalizableOK n (string,int,(),bool,integer,char) + , generalizableOK n (int,(),bool,integer) + , generalizableOK n (int,(),bool,integer,char) + , generalizableOK n (string,int,(),bool,integer,char) -- TODO: implement further tuple instances (7,8,9,10,11,12) and uncomment below ---, generalizableOK n ((),(),(),(),(),(),()) ---, generalizableOK n ((),(),(),(),(),(),(),()) + , generalizableOK n ((),(),(),(),(),(),()) +#if __GLASGOW_HASKELL__ < 710 +-- no 8-tuples for you +#else + , generalizableOK n ((),(),(),(),(),(),(),()) --, generalizableOK n ((),(),(),(),(),(),(),(),()) --, generalizableOK n ((),(),(),(),(),(),(),(),(),()) --, generalizableOK n ((),(),(),(),(),(),(),(),(),(),()) --, generalizableOK n ((),(),(),(),(),(),(),(),(),(),(),()) +#endif -- Silly test, as it basically replicates the actual implementation: , backgroundOf int =$ sort $= [ constant "==" $ (==) -:> int @@ -101,6 +105,58 @@ , not $ mayb int `bgSubset` [mayb [int]] , not $ mayb int `sameNamesIn` [mayb [int]] , not $ mayb int `sameTiersIn` [mayb [int]] + + , generalizations (instances (undefined :: [Int]) []) [expr [0,0::Int]] + == map (:[]) + [ _is + , _i -:- _is + , _i -:- _i -:- _is + , _i -:- _i -:- ll + , _i -:- zero -:- _is + , _i -:- zero -:- ll + , zero -:- _is + , zero -:- _i -:- _is + , zero -:- _i -:- ll + , zero -:- zero -:- _is + ] + + , [ canonicalizeWith (instances (undefined :: [Int]) []) g' + | g <- generalizations (instances (undefined :: [Int]) []) [expr [0,0::Int]] + , g' <- vassignments g ] + == map (:[]) + [ _is + , _i -:- _is + , _i -:- _i -:- _is + , xx -:- xx -:- _is + , _i -:- _i -:- ll + , xx -:- xx -:- ll + , _i -:- zero -:- _is + , _i -:- zero -:- ll + , zero -:- _is + , zero -:- _i -:- _is + , zero -:- _i -:- ll + , zero -:- zero -:- _is + ] + + , candidateConditions (([int] >- bool) `With` MaxConditionSize 3) [xxs] + == [ true, elem' zero xxs ] + + , candidateConditions (([int] >- bool) `With` MaxConditionSize 3) [xx -:- xxs] + =$ sort + $= [ true + , elem' zero xxs + , elem' xx ll + , elem' xx xxs + , zero -/=- xx + , xx -/=- zero + , xx -/=- xx + , zero -<- xx + , xx -<- zero + , xx -<- xx + , zero -<=- xx + , xx -<=- zero + , xx -<=- xx + ] ] listBackgroundOK :: Generalizable a => a -> Bool diff --git a/tests/test-utils.hs b/tests/test-utils.hs new file mode 100644 --- /dev/null +++ b/tests/test-utils.hs @@ -0,0 +1,18 @@ +-- Copyright (c) 2017 Rudy Matela. +-- Distributed under the 3-Clause BSD licence (see the file LICENSE). +import Test +import Test.Extrapolate.Utils + +main :: IO () +main = mainTest tests 1000 + +tests :: Int -> [Bool] +tests n = + [ True + + , holds n $ elemBy (==) ==== elem -:> () + , holds n $ elemBy (==) ==== elem -:> int + , holds n $ elemBy (==) ==== elem -:> bool + , holds n $ elemBy (==) ==== elem -:> [int] + , holds n $ elemBy (==) ==== elem -:> [bool] + ]