Folien 11 Testen mit QuickCheck (.lhs Quellcode)

Dateiinhalt

\nonstopmode
\documentclass[14pt]{scrartcl} % KOMA-Script article

%include polycode.fmt
%% %format . = "."

\usepackage{hyperref}

\title{Functional Programming}
\subtitle{Systematic Testing with QuickCheck}
\author{Andreas Abel, Steffen Jost
 % }\institute{
 \\ LFE Theoretische Informatik, Institut f{\"u}r Informatik,
 \\ Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen}

\date{11 June 2012}

\newcommand{\hidden}[1]{}

\begin{document}
\maketitle

\section{Introduction to QuickCheck}

|QuickCheck| is a Haskell library for automatic testing of logical
program properties, orginally authored by Koen Claessen and John
Hughes (Chalmers University of Technology, 2000).

\begin{code}
import Test.QuickCheck
\end{code}
\hidden{
\begin{code}
import Control.Monad

import System.Random

import Test.QuickCheck.Poly
import Test.QuickCheck.Function
\end{code}
}

\subsection{Properties}

A logical property is an expression of type |Bool|,
it either holds (|True|) or not (|False|).

For example: ``appending the empty list changes nothing''.
\begin{spec}
propAppendNil0 xs = xs ++ [] == xs

t0 = quickCheck propAppendNil0
\end{spec}

Quickcheck answers:
\begin{verbatim}
+++ OK, passed 100 tests.
\end{verbatim}

|propAppendNil0| is not of type |Bool| but of type |a -> Bool|,
thus it is a predicate over type |a|.  Predicates |p| are tested by
generating random values |v| of type |a| and then checking
whether |p v == True|.

Booleans and predicates are instances of |Testable| properties.
\begin{spec}
quickCheck :: Testable prop => prop -> IO ()

class Testable prop where
  property :: prop -> Property

instance Testable Bool
instance (Arbitrary a, Testable prop) => Testable (a -> prop)
\end{spec}

Making a type an instance of |Arbitrary| amounts to writing a
random value generator for this type.  More on this below.

\subsection{Polymorphic Properties}

How come |QuickCheck| knows how to generate values of an unknown type
|a| which occurs in the type of |propAppendNil0|?
\begin{spec}
propAppendNil0 :: [a] -> Bool
\end{spec}

It turns out that unknown types |a| are replaced by the unit type.
\begin{verbatim}
verboseCheck propAppendNil0
Passed:
[]
Passed:
[()]
Passed:
[(),()]
Passed:
[]
...
\end{verbatim}

The values of type |()| are not terribly interesting.  
|QuickCheck| defines wrapper types |A|, |B|, |C| around |Integer|
which we can use instead.
\begin{spec}
import Test.QuickCheck.Poly
\end{spec}
\begin{code}
propAppendNil :: [A] -> Bool
propAppendNil xs = xs ++ [] == xs

t1 = verboseCheck propAppendNil
\end{code}
Now we get:
\begin{verbatim}
Passed:
[]
Passed:
[3]
Passed:
[1,1,2]
...
\end{verbatim}
Module |Poly| also defines types |OrdA|, |OrdB|, and |OrdC| which are
wrappers of |Integer| implementing an |Ord| instance

\subsection{Parametrizing QuickCheck}

We can increase the number of test cases.

\begin{spec}
data Args = Args {
  replay      :: Maybe (StdGen, Int)
  maxSuccess  :: Int
  maxDiscard  :: Int
  maxSize     :: Int
}

stdArgs :: Args

quickCheckWith :: Testable prop => Args -> prop -> IO ()
\end{spec}
\begin{code}
qc1000 = quickCheckWith (stdArgs { maxSuccess = 1000 })
t2 = qc1000 propAppendNil
\end{code}

Another Example: Testing the associativity of append.

\begin{code}
propAppendAssoc :: [A] -> [A] -> [A] -> Bool
propAppendAssoc xs ys zs = (xs ++ ys) ++ zs == xs ++ (ys ++ zs)

t3 = quickCheck propAppendAssoc
\end{code}

\section{Testing Tree Sort}

Tree Sort sorts a list by building a search tree from the list and then flatten it out to a list again by infix traversal.

\begin{code}
data Tree a = Leaf 
            | Node (Tree a) a (Tree a) 
              deriving (Show, Eq)

insert :: Ord a => a -> Tree a -> Tree a
insert a Leaf = Node Leaf a Leaf
insert a (Node l b r) = if a <= b then Node (insert a l) b r
                        else Node l b (insert a r)

toList :: Tree a -> [a]
toList Leaf = []
toList (Node l a r) = toList l ++ a : toList r

sort :: Ord a => [a] -> [a]
sort = toList . foldl (flip insert) Leaf
\end{code}

We can test tree sort always returns a sorted list.

\begin{code}
sorted :: Ord a => [a] -> Bool
sorted []       =  True
sorted [a]      =  True
sorted (a:b:l)  =  a <= b && sorted (b:l)

propTreeSort :: [OrdA] -> Bool
propTreeSort = sorted . sort

t4 = quickCheck propTreeSort
\end{code}

\subsection{Test Case Generators}

We would like to test |insert| by itself.  If we insert something
into a search tree, the result is again a search tree.
This is a conditional/implicational property, one with a precondition.

\begin{spec}
(==>) :: Testable prop => Bool -> prop -> Property

propSortedInsert :: OrdA -> Tree OrdA -> Property
propSortedInsert a t = sortedTree t ==> 
                         sortedTree (insert a t)
\end{spec}

We need to write a test case generator for trees.
That is an expression of type |Gen (Tree a)|, where |Gen| is the |QuickCheck|'s
generator monad.

A generator for a type |a| can be made available under the overloaded
identifier |arbitrary|, if the type is made an instance of |Arbitrary|.
\begin{spec}
class Arbitrary a where
  arbitrary :: Gen a
  ...
\end{spec}

|QuickCheck| offers an extensive library of combinators
for generators, such as |oneof|.

\begin{spec}
import Control.Monad

liftM   :: Monad m => (a -> b) -> (m a -> m b)
liftM3  :: Monad m => (a -> b -> c -> d) -> (m a -> m b -> m c -> m d)
oneof   :: [Gen a] -> Gen a
\end{spec}

\subsection{Generating Unsorted Trees}

Here is a first, naive generator for (unsorted) trees:

\begin{code}
treeGen0 :: (Arbitrary a) => Gen (Tree a)
treeGen0 = oneof  [  return Leaf
                  ,  liftM3 Node treeGen0 arbitrary treeGen0 ]

intTreeGen0 :: Gen (Tree Int)
intTreeGen0 = treeGen0

t5 = sample intTreeGen0
\end{code}

Unfortunately, it is unusable.
|oneof| chooses each alternative with equal probability, thus,
one of each subtrees of |Node| can be expected to be non-empty.
This leads to very large |Tree| instances.

We can control the size of sampled trees using the |sized| combinator..

\begin{spec}
sized :: (Int -> Gen a) -> Gen a
\end{spec}

For size |0| we will now always generate the empty tree, and for size |n| we restrict potential subtrees to size |n-1|.

\begin{code}
treeGen1 :: (Arbitrary a) => Gen (Tree a)
treeGen1 = sized treeGen1'

treeGen1' :: (Arbitrary a) => Int -> Gen (Tree a)
treeGen1' 0 = return Leaf
treeGen1' n = oneof  [  return Leaf
                     ,  liftM3 Node t arbitrary t ]
  where t = treeGen1' (n `div` 2)

intTreeGen1 :: Gen (Tree Int)
intTreeGen1 = treeGen1

t6 = sample intTreeGen1 
\end{code}

Since we generate arbitrary trees, we need to filter out the unsorted ones.
To this end, we check the search tree invariant.

\begin{code}
between :: Ord a => Maybe a -> a -> Maybe a -> Bool
between  Nothing   a  Nothing   = True
between  Nothing   a  (Just r)  = a <= r
between  (Just l)  a  Nothing   = l <= a
between  (Just l)  a  (Just r)  = l <= a && a <= r

betweenTree :: Ord a => Maybe a -> Tree a -> Maybe a -> Bool
betweenTree  ml  Leaf          mr  =   True
betweenTree  ml  (Node l a r)  mr  =   between ml a mr 
                                   &&  betweenTree ml l (Just a)
                                   &&  betweenTree (Just a) r mr 

sortedTree :: Ord a => Tree a -> Bool
sortedTree t = betweenTree Nothing t Nothing
\end{code}

Now we can test that |insert| preserves the search tree invariant.
Property combinator |forAll| let's us supply our custom test case generator.
\begin{spec}
forAll :: (Show a, Testable prop) => Gen a -> (a -> prop) -> Property
\end{spec}

\begin{code}
propSortedInsert :: OrdA -> Property
propSortedInsert a = forAll treeGen1 $ \ t ->
                         sortedTree t ==> 
                           sortedTree (insert a t)

t7 = quickCheck propSortedInsert
\end{code}

\subsection{Test Case Quality}

Analyzing the quality of test cases.

\begin{spec}
classify          -- Conditionally labels test case.
:: Testable prop	
=> Bool	          -- True if the test case should be labelled.
-> String         -- Label.
-> prop	
-> Property	
\end{spec}

How often did we test on the empty tree?

\begin{code}
trivial :: Testable a => Bool -> a -> Property
trivial = (`classify`  "trivial")

propSortedInsert1 :: OrdA -> Property
propSortedInsert1 a = forAll treeGen1 $ \ t ->
                         sortedTree t ==> 
                           (t == Leaf) `trivial` sortedTree (insert a t)

t8 = quickCheck propSortedInsert1
\end{code}

Collecting statistics about the test data.  Here: depth of tested tree.

\begin{code}
depth :: Tree a -> Int
depth Leaf = 0
depth (Node l a r) = 1 + max (depth l) (depth r)

propSortedInsert2 :: OrdA -> Property
propSortedInsert2 a = forAll treeGen1 $ \ t ->
                         sortedTree t ==> 
                           collect (depth t) $ sortedTree (insert a t)

t9 = quickCheck propSortedInsert2
\end{code}

Controlling the probability distribution of generated data.

\begin{spec}
frequency :: [(Int, Gen a)] -> Gen a
\end{spec}

\begin{code}
treeGen2 :: (Arbitrary a) => Gen (Tree a)
treeGen2 = sized treeGen2'

treeGen2' :: (Arbitrary a) => Int -> Gen (Tree a)
treeGen2' 0 = return Leaf
treeGen2' n = frequency  [  (10, return Leaf)
                         ,  (90, liftM3 Node t arbitrary t) ]
  where t = treeGen2' (n `div` 2)

intTreeGen2 :: Gen (Tree Int)
intTreeGen2 = treeGen2

t10 = sample intTreeGen2 

propSortedInsert3 :: OrdA -> Property
propSortedInsert3 a =
  forAll treeGen2 $ \ t ->
    sortedTree t ==> 
      collect (depth t) $ sortedTree (insert a t)

t11 = quickCheck propSortedInsert3
\end{code}

\subsection{Generating Sorted Trees}

The probability that a random tree is a search tree is rather small.
Thus, quickcheck needs to generate a huge number of trees to obtain one
that is suitable for testing |insert|.  This is rather wasteful.

Let us define a generator for sorted trees instead!

\begin{spec}
import System.Random
\end{spec}
\begin{code}
sortedTreeGen :: (Arbitrary a, Bounded a, Random a) => Gen (Tree a)
sortedTreeGen = sized $ \ n -> sortedTreeGen' n (minBound, maxBound)

sortedTreeGen' :: (Arbitrary a, Random a) => Int -> (a, a) -> Gen (Tree a)
sortedTreeGen' 0  _      = return Leaf
sortedTreeGen' n  (l,r)  = 
  frequency  [  (10,  return Leaf)
             ,  (90,  do  a <- choose (l,r)
                          let n' = n `div` 2
                          tl  <- sortedTreeGen' n' (l,a)
                          tr  <- sortedTreeGen' n' (a,r)
                          return $ Node tl a tr) ]

sortedIntTreeGen :: Gen (Tree Int)
sortedIntTreeGen = sortedTreeGen

t12 = sample sortedIntTreeGen 

propSortedInsert4 :: Int -> Property
propSortedInsert4 a =
  forAll sortedTreeGen $ \ t ->
    collect (depth t) $ sortedTree (insert a t)

t13 = quickCheck propSortedInsert4
\end{code}


\subsection{Instantiating the |Arbitrary| Class}

We make the generator for unordered |Tree|s available as instance of
|Arbitrary|.
\begin{spec}
class Arbitrary a where
  arbitrary :: Gen a
  shrink :: a -> [a]
\end{spec}

Class |Arbitrary| suggest to also define a test case shrinker.
If |quickCheck| finds a counterexample to a property, it will
repeatedly |shrink| it as long as it stays a counterexample.
Small counterexamples make bug finding a lot easier!
|shrink t| should return all immediate proper subtrees of |t|.

\begin{code}
instance (Arbitrary a) => Arbitrary (Tree a) where
  arbitrary = treeGen2
  shrink (Leaf)        = []
  shrink (Node l a r)  = [l,r]
  
propSortedInsert5 :: OrdA -> Tree OrdA -> Property
propSortedInsert5 a t = sortedTree t ==> 
                           collect (depth t) $ sortedTree (insert a t)

t14 = quickCheck propSortedInsert5
\end{code}

We would also like to expose the generator for sorted trees.
But there cannot be two instances of a type class for the same type!
We help ourselves by a |newtype| wrapper.

\begin{code}
newtype SortedTree a =  SortedTree { tree :: (Tree a) } deriving (Show, Eq)

instance (Arbitrary a, Random a, Bounded a) => Arbitrary (SortedTree a) where
  arbitrary = liftM SortedTree sortedTreeGen
  shrink (SortedTree (Leaf))        = []
  shrink (SortedTree (Node l a r))  = [SortedTree l, SortedTree r]

propSortedInsert6 :: Int -> SortedTree Int -> Property
propSortedInsert6 a (SortedTree t) = 
  collect (depth t) $ sortedTree (insert a t)

t15 = quickCheck propSortedInsert6
\end{code}


\section{Generating Random Functions}

Testing higher-order functions such as |map| requires the generation of
random functions.
\begin{code}
prop_map_comp :: Blind (A -> B) -> Blind (B -> C) -> [A] -> Bool
prop_map_comp (Blind f) (Blind g) xs = map g (map f xs) == map (g . f) xs  

t16 = quickCheck prop_map_comp
\end{code}
|Blind| means that there is no |Show| instance, i.e., we cannot see
on which functions the test case fails.

How does |QuickCheck| generate random functions?

\subsection{The |CoArbitrary| Class}

A function of type |a -> b| should not return the same |b| for all |a|.
It should return different |b|s for different |a|s, at least in some
or most cases.

|QuickCheck| achieves this by changing the seed of the random generator
by composing it with the function argument, before randomly generating
a function result.  To this end, the function argument has to be
casted into an |Integral| value that can be mixed into the random seed.

The job of perturbing the random seed is done for us by library function
|variant|:
\begin{spec}
variant :: Integral n => n -> Gen a -> Gen a
\end{spec}

If we want to generate functions over our own types |a|, we have to make
them instances of |CoArbitrary|.
\begin{spec}
class CoArbitrary a where
  coarbitrary :: a -> Gen c -> Gen c
\end{spec}

|QuickCheck| offers a standard implementation for ``lazy people''"
\begin{spec}
coarbitraryShow :: Show a => a -> Gen b -> Gen b
\end{spec}

If we have a |Show| instance for our type |T| we get the |CoArbitrary| instance simply by.
\begin{spec}
instance CoArbitrary T where
  coarbitrary = coarbitraryShow
\end{spec}
This will |show| values of type |T|, then cast them to an |Integral| which will then act on the random seed.

\subsection{Printable Functions}

|QuickCheck| also offers generation of functions that can
be printed as argument-result-tables.

\begin{spec}
import Test.QuickCheck.Function
\end{spec}

\begin{code}
prop_idempot :: Fun Integer Integer -> Integer -> Bool
prop_idempot (Fun _ f) x = f (f x) == f x 

t20 = quickCheck prop_idempot
\end{code}

Here we might get:
\begin{verbatim}
*** Failed! Falsifiable (after 4 tests and 7 shrinks):  
{0->1, _->0}
0
\end{verbatim}
Which means that the function that maps |0| to |1| and everything
else to |0| is not idempotent.

The library offers us a type |Fun a b| for functions from |a| to |b|
that have a concrete representation |a :-> b|, a default value |b|,
and the actual function |a -> b|.
\begin{spec}
data Fun a b = Fun (a :-> b, b) (a -> b)
\end{spec}
The concrete representation could be just a input-output table.
For details, see library documentation.


\section{Testing Stateful Code}

The paper
\begin{quote}
Koen Classen and John Hughes \\
\emph{Testing Monadic Code with QuickCheck} \\
Haskell Workshop 2002
\end{quote}
demonstrates how to test stateful code.

% Let us assume we want to test laws of an imperative stack


\end{document}