QuickCheck properties for IntSet

David Benbennick dbenbenn at gmail.com
Sun Dec 9 04:25:48 EST 2007


On 12/8/07, David Benbennick <dbenbenn at gmail.com> wrote:
> I commented out some code that could never be executed:
> * Some case-statement cases that could never occur.
> * >>= for the Identity monad used internally.

Sorry, I forgot to run the "validate" script on the previous patch.
Turns out validate requires >>= to be explicitly set, even though it
isn't used.  New patch bundle is attached.

This version also removes an unused function, and adds a QuickCheck
property for dataTypeOf.
-------------- next part --------------

New patches:

[IntSet QuickCheck properties
David Benbennick <dbenbenn at gmail.com>**20071203040728
 
 1) Remove foldlStrict, and use Data.List.foldl' instead.
 2) Add many QuickCheck properties, checking almost
    every exported function of IntSet.
] {
hunk ./Data/IntSet.hs 114
-import List (nub,sort)
-import qualified List
hunk ./Data/IntSet.hs 115
+import qualified Prelude
hunk ./Data/IntSet.hs 315
-  = foldlStrict union empty xs
+  = List.foldl' union empty xs
hunk ./Data/IntSet.hs 410
+-- Return LT if t1 is a proper subset of t2,
+-- EQ if t1 == t2, and GT otherwise.
hunk ./Data/IntSet.hs 677
-  = foldlStrict ins empty xs
+  = List.foldl' ins empty xs
hunk ./Data/IntSet.hs 942
-{--------------------------------------------------------------------
-  Utilities 
---------------------------------------------------------------------}
-foldlStrict f z xs
-  = case xs of
-      []     -> z
-      (x:xx) -> let z' = f z x in seq z' (foldlStrict f z' xx)
-
-
hunk ./Data/IntSet.hs 943
-{--------------------------------------------------------------------
-  Testing
---------------------------------------------------------------------}
-testTree :: [Int] -> IntSet
-testTree xs   = fromList xs
-test1 = testTree [1..20]
-test2 = testTree [30,29..10]
-test3 = testTree [1,4,6,89,2323,53,43,234,5,79,12,9,24,9,8,423,8,42,4,8,9,3]
-
hunk ./Data/IntSet.hs 961
-  arbitrary = do{ xs <- arbitrary
-                ; return (fromList xs)
-                }
+  arbitrary = arbitrary >>= return . fromList
+  coarbitrary Nil = variant 0
+  coarbitrary (Tip x) = variant 1 . coarbitrary x
+  coarbitrary (Bin _ _ left right) = variant 2 . coarbitrary left . coarbitrary right
hunk ./Data/IntSet.hs 997
-    == List.sort ((List.\\) (nub xs)  (nub ys))
+    == List.sort ((List.\\) (List.nub xs)  (List.nub ys))
hunk ./Data/IntSet.hs 1002
-    == List.sort (nub ((List.intersect) (xs)  (ys)))
+    == List.sort (List.nub ((List.intersect) (xs)  (ys)))
hunk ./Data/IntSet.hs 1014
-  = (sort (nub xs) == toAscList (fromList xs))
+  = (List.sort (List.nub xs) == toAscList (fromList xs))
hunk ./Data/IntSet.hs 1017
-  Bin invariants
+  Check that after every operation, an IntSet satisfies its invariants
hunk ./Data/IntSet.hs 1019
-powersOf2 :: IntSet
-powersOf2 = fromList [2^i | i <- [0..63]]
+isValid Nil = True
+isValid s = isValid' s where
+  isValid' (Tip _) = True
+  isValid' Nil = False
+  isValid' s@(Bin prefix msk left right) = checkPrefix s && isPow2 msk && checkLeftRight s && isValid' left && isValid' right
hunk ./Data/IntSet.hs 1025
--- Check the invariant that the mask is a power of 2.
-prop_MaskPow2 :: IntSet -> Bool
-prop_MaskPow2 (Bin _ msk left right) = member msk powersOf2 && prop_MaskPow2 left && prop_MaskPow2 right
-prop_MaskPow2 _ = True
+  -- Check that the prefix satisfies its invariant.
+  checkPrefix s@(Bin prefix msk _ _) = all (\elem -> match elem prefix msk) $ toList s
hunk ./Data/IntSet.hs 1028
--- Check that the prefix satisfies its invariant.
-prop_Prefix :: IntSet -> Bool
-prop_Prefix s@(Bin prefix msk left right) = all (\elem -> match elem prefix msk) (toList s) && prop_Prefix left && prop_Prefix right
-prop_Prefix _ = True
+  isPow2 x = x .&. (x - 1) == 0
hunk ./Data/IntSet.hs 1030
--- Check that the left elements don't have the mask bit set, and the right
--- ones do.
-prop_LeftRight :: IntSet -> Bool
-prop_LeftRight (Bin _ msk left right) = and [x .&. msk == 0 | x <- toList left] && and [x .&. msk == msk | x <- toList right]
-prop_LeftRight _ = True
+  -- Check that the left elements don't have the mask bit set, and the right
+  -- ones do.
+  checkLeftRight (Bin _ msk left right) = and [x .&. msk == 0 | x <- toList left] && and [x .&. msk == msk | x <- toList right]
+
+prop_valid_bkbk a b = isValid $ a \\ b
+prop_valid_empty = isValid empty
+prop_valid_singleton a = isValid $ singleton a
+prop_valid_insert a b = isValid $ insert a b
+prop_valid_delete a b = isValid $ delete a b
+prop_valid_union a b = isValid $ union a b
+prop_valid_unions a = isValid $ unions a
+prop_valid_difference a b = isValid $ difference a b
+prop_valid_intersection a b = isValid $ intersection a b
+prop_valid_filter a b = isValid $ filter a b
+prop_valid_partition a b = all isValid [x, y] where
+  (x, y) = partition a b
+prop_valid_split a b = all isValid [x, y] where
+  (x, y) = split a b
+prop_valid_splitMember a b = all isValid [x, y] where
+  (x, _, y) = splitMember a b
+prop_valid_deleteMin a = not (null a) ==> isValid (deleteMin a)
+prop_valid_deleteMax a = not (null a) ==> isValid (deleteMax a)
+prop_valid_deleteFindMin a = not (null a) ==> isValid (snd $ deleteFindMin a)
+prop_valid_deleteFindMax a = not (null a) ==> isValid (snd $ deleteFindMax a)
+prop_valid_maxView a = all (isValid . snd) $ maxView a
+prop_valid_minView a = all (isValid . snd) $ minView a
+prop_valid_map a b = isValid $ map a b
+prop_valid_fromList a = isValid $ fromList a
+prop_valid_fromAscList a = isValid $ fromAscList b where
+  b = List.sort a
+prop_valid_fromDistinctAscList a = isValid $ fromDistinctAscList b where
+  b = toList a
hunk ./Data/IntSet.hs 1064
-  IntSet operations are like Set operations
+  IntSet functions are like Set functions
hunk ./Data/IntSet.hs 1066
+-- Helper
hunk ./Data/IntSet.hs 1070
--- Check that IntSet.isProperSubsetOf is the same as Set.isProperSubsetOf.
+-- Check the helper is right
+prop_toSet :: IntSet -> Bool
+prop_toSet a = a == fromList (Set.toList $ toSet a)
+
+prop_bkbk :: IntSet -> IntSet -> Bool
+prop_bkbk a b = toSet (a \\ b) == (toSet a) Set.\\ (toSet b)
+
+prop_null :: IntSet -> Bool
+prop_null a = null a == Set.null (toSet a)
+
+prop_size :: IntSet -> Bool
+prop_size a = size a == Set.size (toSet a)
+
+prop_member :: Int -> IntSet -> Bool
+prop_member a b = member a b == Set.member a (toSet b)
+
+prop_notMember :: Int -> IntSet -> Bool
+prop_notMember a b = notMember a b == Set.notMember a (toSet b)
+
+-- For testing isSubsetOf and isProperSubsetOf:
+-- Given two random sets a and b, it is very unlikely that a is a subset of b.
+-- So prop_isSubsetOf only checks the "False" case.
+-- prop_isSubsetOf2 manufactures the "True" case.
+prop_isSubsetOf :: IntSet -> IntSet -> Bool
+prop_isSubsetOf a b = isSubsetOf a b == Set.isSubsetOf (toSet a) (toSet b)
+
+prop_isSubsetOf2 :: IntSet -> IntSet -> Bool
+prop_isSubsetOf2 a b = isSubsetOf a c == Set.isSubsetOf (toSet a) (toSet c) where
+  c = union a b
+
hunk ./Data/IntSet.hs 1103
--- In the above test, isProperSubsetOf almost always returns False (since a
--- random set is almost never a subset of another random set).  So this second
--- test checks the True case.
hunk ./Data/IntSet.hs 1106
+
+prop_empty :: Bool
+prop_empty = toSet empty == Set.empty
+
+prop_singleton :: Int -> Bool
+prop_singleton a = toSet (singleton a) == Set.singleton a
+
+prop_insert :: Int -> IntSet -> Bool
+prop_insert a b = toSet (insert a b) == Set.insert a (toSet b)
+
+prop_delete :: Int -> IntSet -> Bool
+prop_delete a b = toSet (delete a b) == Set.delete a (toSet b)
+
+prop_union :: IntSet -> IntSet -> Bool
+prop_union a b = toSet (union a b) == Set.union (toSet a) (toSet b)
+
+prop_unions :: [IntSet] -> Bool
+prop_unions a = toSet (unions a) == Set.unions (Prelude.map toSet a)
+
+prop_difference :: IntSet -> IntSet -> Bool
+prop_difference a b = toSet (difference a b) == Set.difference (toSet a) (toSet b)
+
+prop_intersection :: IntSet -> IntSet -> Bool
+prop_intersection a b = toSet (intersection a b) == Set.intersection (toSet a) (toSet b)
+
+instance Show (Int -> Bool) where
+  show _ = "<function :: Int -> Bool>"
+instance Show (Int -> Int) where
+  show _ = "<function :: Int -> Int>"
+instance Show (Int -> Int -> Int) where
+  show _ = "<function :: Int -> Int -> Int>"
+instance Arbitrary Char where
+  arbitrary = choose ('\0', '\255')
+
+prop_filter :: (Int -> Bool) -> IntSet -> Bool
+prop_filter a b = toSet c == Set.filter a (toSet b) where
+  c = filter a b
+
+prop_partition :: (Int -> Bool) -> IntSet -> Bool
+prop_partition a b = (toSet c, toSet d) == Set.partition a (toSet b) where
+  (c, d) = partition a b
+
+prop_split :: Int -> IntSet -> Bool
+prop_split a b = (toSet x, toSet z) == Set.split a (toSet b) where
+  (x, z) = split a b
+
+prop_splitMember :: Int -> IntSet -> Bool
+prop_splitMember a b = (toSet x, y, toSet z) == Set.splitMember a (toSet b) where
+  (x, y, z) = splitMember a b
+
+prop_findMin :: IntSet -> Property
+prop_findMin a = not (null a) ==> findMin a == Set.findMin (toSet a)
+
+prop_findMax :: IntSet -> Property
+prop_findMax a = not (null a) ==> findMax a == Set.findMax (toSet a)
+
+prop_deleteMin :: IntSet -> Property
+prop_deleteMin a = not (null a) ==> toSet (deleteMin a) == Set.deleteMin (toSet a)
+
+prop_deleteMax :: IntSet -> Property
+prop_deleteMax a = not (null a) ==> toSet (deleteMax a) == Set.deleteMax (toSet a)
+
+prop_deleteFindMin :: IntSet -> Property
+prop_deleteFindMin a = not (null a) ==> (x, toSet y) == Set.deleteFindMin (toSet a) where
+  (x, y) = deleteFindMin a
+
+prop_deleteFindMax :: IntSet -> Property
+prop_deleteFindMax a = not (null a) ==> (x, toSet y) == Set.deleteFindMax (toSet a) where
+  (x, y) = deleteFindMax a
+
+prop_maxView :: IntSet -> Bool
+prop_maxView a = Prelude.map (\(x, y) -> (x, toSet y)) (maxView a) == Set.maxView (toSet a)
+
+prop_minView :: IntSet -> Bool
+prop_minView a = Prelude.map (\(x, y) -> (x, toSet y)) (minView a) == Set.minView (toSet a)
+
+prop_map :: (Int -> Int) -> IntSet -> Bool
+prop_map a b = toSet (map a b) == Set.map a (toSet b)
+
+prop_fold :: (Int -> Int -> Int) -> Int -> IntSet -> Bool
+prop_fold a b c = fold a b c == Set.fold a b (toSet c)
+
+-- The documentation for fold asserts this test.
+prop_fold2 :: IntSet -> Bool
+prop_fold2 set = elems set == fold (:) [] set
+
+prop_elems :: IntSet -> Bool
+prop_elems a = elems a == Set.elems (toSet a)
+
+prop_toList :: IntSet -> Bool
+prop_toList a = toList a == Set.toList (toSet a)
+
+prop_fromList :: [Int] -> Bool
+prop_fromList a = toSet (fromList a) == Set.fromList a
+
+prop_toAscList :: IntSet -> Bool
+prop_toAscList a = toAscList a == Set.toAscList (toSet a)
+
+prop_fromAscList :: [Int] -> Bool
+prop_fromAscList a = toSet (fromAscList b) == Set.fromAscList b where
+  b = List.sort a
+
+prop_fromDistinctAscList :: IntSet -> Bool
+prop_fromDistinctAscList a = toSet (fromDistinctAscList b) == Set.fromDistinctAscList b where
+  b = toAscList a 
+
+prop_compare :: IntSet -> IntSet -> Bool
+prop_compare a b = compare a b == compare (toSet a) (toSet b)
+
+prop_showsPrec :: Int -> IntSet -> String -> Bool
+prop_showsPrec a b c = showsPrec a b c == showsPrec a (toSet b) c
+
+test_all = do
+  qcheck prop_Single
+  qcheck prop_InsertDelete
+  qcheck prop_UnionInsert
+  qcheck prop_UnionAssoc
+  qcheck prop_UnionComm
+  qcheck prop_Diff
+  qcheck prop_Int
+  qcheck prop_Ordered
+  qcheck prop_List
+  qcheck prop_toSet
+  qcheck prop_bkbk
+  qcheck prop_null
+  qcheck prop_size
+  qcheck prop_member
+  qcheck prop_notMember
+  qcheck prop_isSubsetOf
+  qcheck prop_isSubsetOf2
+  qcheck prop_isProperSubsetOf
+  qcheck prop_isProperSubsetOf2
+  qcheck prop_empty
+  qcheck prop_singleton
+  qcheck prop_insert
+  qcheck prop_delete
+  qcheck prop_union
+  qcheck prop_unions
+  qcheck prop_difference
+  qcheck prop_intersection
+  qcheck prop_filter
+  qcheck prop_partition
+  qcheck prop_split
+  qcheck prop_splitMember
+  qcheck prop_findMin
+  qcheck prop_findMax
+  qcheck prop_deleteMin
+  qcheck prop_deleteMax
+  qcheck prop_deleteFindMin
+  qcheck prop_deleteFindMax
+  qcheck prop_maxView
+  qcheck prop_minView
+  qcheck prop_map
+  qcheck prop_fold
+  qcheck prop_fold2
+  qcheck prop_elems
+  qcheck prop_toList
+  qcheck prop_fromList
+  qcheck prop_toAscList
+  qcheck prop_fromAscList
+  qcheck prop_fromDistinctAscList
+  qcheck prop_compare
+  qcheck prop_showsPrec
+  qcheck prop_valid_bkbk
+  qcheck prop_valid_empty
+  qcheck prop_valid_singleton
+  qcheck prop_valid_insert
+  qcheck prop_valid_delete
+  qcheck prop_valid_union
+  qcheck prop_valid_unions
+  qcheck prop_valid_difference
+  qcheck prop_valid_intersection
+  qcheck prop_valid_filter
+  qcheck prop_valid_partition
+  qcheck prop_valid_split
+  qcheck prop_valid_splitMember
+  qcheck prop_valid_deleteMin
+  qcheck prop_valid_deleteMax
+  qcheck prop_valid_deleteFindMin
+  qcheck prop_valid_deleteFindMax
+  qcheck prop_valid_maxView
+  qcheck prop_valid_minView
+  qcheck prop_valid_map
+  qcheck prop_valid_fromList
+  qcheck prop_valid_fromAscList
+  qcheck prop_valid_fromDistinctAscList
}

[more QuickCheck properties
David Benbennick <dbenbenn at gmail.com>**20071208093646
 
 Add more QuickCheck properties.  The only code that remains untested is
 1) The Data instance
 2) The debugging functions that print IntSets in various ways
 
 Also remove insertR: the documentation doesn't specify "right bias" for union, and in any case "right bias" doesn't mean anything for an IntSet.
 
 And comment out 4 lines of code that could never be executed.
] {
hunk ./Data/IntSet.hs 281
--- right-biased insertion, used by 'union'
-insertR :: Int -> IntSet -> IntSet
-insertR x t
-  = case t of
-      Bin p m l r 
-        | nomatch x p m -> join x (Tip x) p t
-        | zero x m      -> Bin p m (insert x l) r
-        | otherwise     -> Bin p m l (insert x r)
-      Tip y 
-        | x==y          -> t
-        | otherwise     -> join x (Tip x) y t
-      Nil -> Tip x
-
hunk ./Data/IntSet.hs 322
-union t (Tip x) = insertR x t  -- right bias
+union t (Tip x) = insert x t  -- right bias
hunk ./Data/IntSet.hs 499
-      Nil -> (Nil,Nil)
+      -- Nil -> (Nil,Nil)   -- This case can't happen.
hunk ./Data/IntSet.hs 529
-      Nil -> (Nil,False,Nil)
+      -- Nil -> (Nil,False,Nil)  -- This case can't happen
hunk ./Data/IntSet.hs 572
-	m >>= k  = k (runIdentity m)
+	-- m >>= k  = k (runIdentity m)  -- Not used
hunk ./Data/IntSet.hs 639
-      Nil         -> z
+      -- Nil         -> z  -- This case can't happen
hunk ./Data/IntSet.hs 1064
+prop_mempty :: Bool
+prop_mempty = toSet mempty == mempty
+
+prop_mappend :: IntSet -> IntSet -> Bool
+prop_mappend a b = toSet (mappend a b) == mappend (toSet a) (toSet b)
+
+prop_mconcat :: [IntSet] -> Bool
+prop_mconcat a = toSet (mconcat a) == mconcat (Prelude.map toSet a)
+
hunk ./Data/IntSet.hs 1211
+prop_equal :: IntSet -> IntSet -> Bool
+prop_equal a b = (a == b) == (toSet a == toSet b)
+
+prop_nequal :: IntSet -> IntSet -> Bool
+prop_nequal a b = (a /= b) == (toSet a /= toSet b)
+
hunk ./Data/IntSet.hs 1220
+prop_show :: IntSet -> Bool
+prop_show a = show a == show (toSet a)
+
+prop_read :: IntSet -> Bool
+prop_read a = read (show a) == a
+
+prop_readList :: [IntSet] -> Bool
+prop_readList a = readList (show a) == [(a, "")]
+
+prop_typeOf :: IntSet -> Bool
+prop_typeOf a = show (typeOf a) == "IntSet"
+
+data Error a = Error String deriving Eq
+instance Monad Error where
+  fail s = Error s
+
+prop_maxView_error :: Bool
+prop_maxView_error = maxView empty == Error "maxView: empty set has no maximal element"
+
+prop_minView_error :: Bool
+prop_minView_error = minView empty == Error "minView: empty set has no minimal element"
+
hunk ./Data/IntSet.hs 1254
+  qcheck prop_mempty
+  qcheck prop_mappend
+  qcheck prop_mconcat
hunk ./Data/IntSet.hs 1295
+  qcheck prop_equal
+  qcheck prop_nequal
hunk ./Data/IntSet.hs 1298
+  qcheck prop_show
+  qcheck prop_read
+  qcheck prop_readList
+  qcheck prop_typeOf
+  qcheck prop_maxView_error
+  qcheck prop_minView_error
}

[Remove explicit instance of Eq, use deriving instead
David Benbennick <dbenbenn at gmail.com>**20071208094555] {
hunk ./Data/IntSet.hs 169
+  deriving Eq
hunk ./Data/IntSet.hs 679
-
-{--------------------------------------------------------------------
-  Eq 
---------------------------------------------------------------------}
-instance Eq IntSet where
-  t1 == t2  = equal t1 t2
-  t1 /= t2  = nequal t1 t2
-
-equal :: IntSet -> IntSet -> Bool
-equal (Bin p1 m1 l1 r1) (Bin p2 m2 l2 r2)
-  = (m1 == m2) && (p1 == p2) && (equal l1 l2) && (equal r1 r2) 
-equal (Tip x) (Tip y)
-  = (x==y)
-equal Nil Nil = True
-equal t1 t2   = False
-
-nequal :: IntSet -> IntSet -> Bool
-nequal (Bin p1 m1 l1 r1) (Bin p2 m2 l2 r2)
-  = (m1 /= m2) || (p1 /= p2) || (nequal l1 l2) || (nequal r1 r2) 
-nequal (Tip x) (Tip y)
-  = (x/=y)
-nequal Nil Nil = False
-nequal t1 t2   = True
-
}

[Better prop_typeOf test
David Benbennick <dbenbenn at gmail.com>**20071208095158] {
hunk ./Data/IntSet.hs 1206
-prop_typeOf :: IntSet -> Bool
-prop_typeOf a = show (typeOf a) == "IntSet"
+prop_typeOf :: Bool
+prop_typeOf = show (typeOf (undefined :: IntSet)) == "IntSet"
}

[Remove obsolete comment
David Benbennick <dbenbenn at gmail.com>**20071208100137] {
hunk ./Data/IntSet.hs 323
-union t (Tip x) = insert x t  -- right bias
+union t (Tip x) = insert x t
}

[Remove meaningless "left-biasing" code
David Benbennick <dbenbenn at gmail.com>**20071208103316] {
hunk ./Data/IntSet.hs 104
-import Prelude hiding (lookup,filter,foldr,foldl,null,map)
+import Prelude hiding (filter,foldr,foldl,null,map)
hunk ./Data/IntSet.hs 235
--- 'lookup' is used by 'intersection' for left-biasing
-lookup :: Int -> IntSet -> Maybe Int
-lookup k t
-  = let nk = natFromInt k  in seq nk (lookupN nk t)
-
-lookupN :: Nat -> IntSet -> Maybe Int
-lookupN k t
-  = case t of
-      Bin p m l r 
-        | zeroN k (natFromInt m) -> lookupN k l
-        | otherwise              -> lookupN k r
-      Tip kx 
-        | (k == natFromInt kx)  -> Just kx
-        | otherwise             -> Nothing
-      Nil -> Nothing
-
hunk ./Data/IntSet.hs 363
-intersection t (Tip x) 
-  = case lookup x t of
-      Just y  -> Tip y
-      Nothing -> Nil
+intersection t1 t2@(Tip x)
+  | member x t1  = t2
+  | otherwise    = Nil
}

[validate script requires this to be explicit
David Benbennick <dbenbenn at gmail.com>**20071209082636] {
hunk ./Data/IntSet.hs 556
-	-- m >>= k  = k (runIdentity m)  -- Not used
+	m >>= k  = undefined   -- This is not used, but it could be: = k (runIdentity m)
}

[Remove unused zeroN, add QuickCheck for dataTypeOf
David Benbennick <dbenbenn at gmail.com>**20071209091042] {
hunk ./Data/IntSet.hs 114
+import qualified Data.Generics as Generics
hunk ./Data/IntSet.hs 819
-zeroN :: Nat -> Nat -> Bool
-zeroN i m = (i .&. m) == 0
-
hunk ./Data/IntSet.hs 1200
+prop_dataTypeOf :: Bool
+prop_dataTypeOf = Generics.dataTypeName b == "Data.IntSet.IntSet" && Generics.dataTypeRep b == Generics.NoRep where
+  b = dataTypeOf (undefined :: IntSet)
+
hunk ./Data/IntSet.hs 1289
+  qcheck prop_dataTypeOf
}

Context:

[Fix a link in haddock docs
Ian Lynagh <igloo at earth.li>**20071126184450] 
[Fix some URLs
Ian Lynagh <igloo at earth.li>**20071126214233] 
[Add tiny regression test
David Benbennick <dbenbenn at gmail.com>**20071113045358] 
[Fix ticket 1762
David Benbennick <dbenbenn at gmail.com>**20071111201939] 
[Specify build-type: Simple
Duncan Coutts <duncan at haskell.org>**20071018125404] 
[Add a boring file
Ian Lynagh <igloo at earth.li>**20070913204647] 
[TAG 2007-09-13
Ian Lynagh <igloo at earth.li>**20070913215901] 
Patch bundle hash:
c11b8ffb201b72f85467aecf56e60bf723eb5544


More information about the Libraries mailing list