files/practicum/StdSetTest.icl

   1 module StdSetTest
   2
   3 /*      Test module StdSet
   4         Voor werken met Gast:
   5                 (*) gebruik Environment 'Gast'
   6                 (*) zet Project Options op 'Basic Values Only' en '8M' Maximum Heap Size.
   7 */
   8
   9 import gast
  10 import GenLexOrd
  11 import StdSet
  12
  13 Start = testn 2000
  14         (\n` n2` m -> let n  = cast [A,B,C] n`
  15                           n2 = cast [A,B,C] n2`
  16                        in
  17                                                         membership            m n  /\
  18                                                         conversion_invariant  n    /\
  19                                                         length_property       n    /\
  20                                                         subset_property       n n2 /\
  21                                                         strictsubset_property n n2 /\
  22                                                         empty_properties      m n  /\
  23                                                         disjoint_properties   n n2 /\
  24                                                         product_properties    n n2 /\
  25                                                         intersect_properties  n n2 /\
  26                                                         setminus_properties   n n2 /\
  27                                                         union_properties      n n2 /\
  28                                                         powset_properties     n    /\
  29                                                         True
  30                    )
  31
  32 :: Enum = A | B | C
  33
  34 derive bimap []
  35 derive ggen Enum
  36 derive genShow Enum
  37 derive gEq Enum
  38 derive gLexOrd Enum
  39 instance == Enum where (==) x y = gEq{|*|} x y
  40 instance <  Enum where  (<) x y = gEq{|*|} (gLexOrd{|*|} x y) LT
  41
  42 // clean should have something like this!
  43 cast :: a a -> a
  44 cast _ x = x
  45
  46 membership :: Enum [Enum] -> Property
  47 membership x xs
  48  = name "membership"
  49    ( memberOfSet x s <==> isMember x xs )
  50   where s = toSet xs
  51
  52 conversion_invariant :: [Enum] -> Property
  53 conversion_invariant xs
  54  = name "conversion_invariant"
  55    ( toSet (fromSet xs`) == xs` )
  56    where xs` = toSet xs
  57
  58 length_property :: [Enum] -> Property
  59 length_property xs
  60  = name "length_property"
  61    ( nrOfElements s == length (removeDup xs) )
  62  where s = toSet xs
  63
  64 subset_property :: [Enum] [Enum] -> Property
  65 subset_property xs ys
  66  = name "subset_property"
  67    ( (isSubset u v) <==> all (flip isMember ys) xs)
  68   where (u,v) = (toSet xs, toSet ys)
  69
  70 strictsubset_property :: [Enum] [Enum] -> Property
  71 strictsubset_property xs ys
  72  = name "strictsubset_property"
  73    ( (isStrictSubset u v) <==> (all (flip isMember ys) xs && not (all (flip isMember xs) ys)) )
  74   where (u,v) = (toSet xs, toSet ys)
  75
  76 // everything you alwys wanted to know about the empty set...
  77 // ... but were afraid to ask
  78 empty_properties :: Enum [Enum] -> Property
  79 empty_properties x xs
  80  = name "empty_properties"
  81    ( isEmptySet (cast dummy zero) /\ isEmptySet (toSet (cast [A] [])) /\
  82      ((nrOfElements s == 0) <==> isEmptySet s) /\
  83            ((zero == s)     <==> isEmptySet s) )
  84  where s = toSet xs
  85        dummy :: Set Enum
  86        dummy = undef
  87
  88 product_properties :: [Enum] [Enum] -> Property
  89 product_properties xs ys
  90  = name "product_properties"
  91    ( product u v == toSet [(x,y) \\ x<-xs, y<-ys ] )
  92  where (u,v) = (toSet xs, toSet ys)
  93
  94 powset_properties :: [Enum] -> Property
  95 powset_properties xs
  96  = name "powset_properties"
  97    ( powerSet s == toSet (map toSet (subs xs)) )
  98  where s = toSet xs
  99        subs [] = [[]]
 100        subs [x:xs] = subs xs ++ [ [x:xs`] \\ xs` <- subs xs ]
 101
 102 union_properties :: [Enum] [Enum] -> Property
 103 union_properties xs ys
 104  = name "union_properties"
 105    ( union u v == toSet (xs++ys) )
 106  where (u,v) = (toSet xs, toSet ys)
 107
 108 intersect_properties :: [Enum] [Enum] -> Property
 109 intersect_properties xs ys
 110  = name "intersect_properties"
 111    ( intersection u v == toSet [ x \\ x<-xs | isMember x ys ] )
 112  where (u,v) = (toSet xs, toSet ys)
 113
 114 setminus_properties :: [Enum] [Enum] -> Property
 115 setminus_properties xs ys
 116  = name "setminus_properties"
 117    ( without u v == toSet [ x \\ x<-xs | not (isMember x ys) ])
 118  where (u,v) = (toSet xs, toSet ys)
 119
 120 disjoint_properties :: [Enum] [Enum] -> Property
 121 disjoint_properties xs ys
 122  = name "disjoint_properties"
 123    ( isDisjoint u v <==> (nrOfElements u + nrOfElements v == nrOfElements (union u v)) )
 124  where (u,v) = (toSet xs, toSet ys)