afp/a12/testCash.icl

   1 module testCash
   2
   3 import cashModel
   4 import gastyStart
   5
   6 //gen{|Euro|} = [f {euro=e,cent=c}\\e<-[0..], c <- [0..99], f<-[id,(~)]]
   7 gen{|Euro|} = [f {euro=e,cent=c}\\e<-[0..], c <- merge [0..50] [51..99], f<-[id,(~)]]
   8 where
   9         merge [a:x] ys = [a:merge ys x]
  10         merge [] ys =ys
  11 derive string Euro, Product, []
  12 derive gen Product, []
  13 derive bimap []
  14 derive gEq Product
  15
  16 pPlusAssociative :: Euro Euro Euro -> Equ
  17 pPlusAssociative a b c = a + (b + c) =.= (a + b) + c
  18
  19 pPlusCommutative :: Euro Euro -> Equ
  20 pPlusCommutative a b = a + b =.= b + a
  21
  22 pPlusIdentity :: Euro -> Equ
  23 pPlusIdentity i = i + zero =.= i
  24
  25 pNegSub :: Euro -> Equ
  26 pNegSub i = zero - i =.= ~i
  27
  28 pNegNegId :: Euro -> Equ
  29 pNegNegId i = ~ (~i) =.= i
  30
  31 //model :: [Product] Action -> ([Product],[Euro])
  32 pFair :: [Product] Product -> Equ
  33 pFair state p = euro state =.= euro t - euro o
  34 where
  35         (t,o) = model state (Rem p)
  36 //
  37 //pFair2 :: [Product] Action -> Equ //Euro
  38 //pFair2 state action = euro state =.= euro t - euro o
  39 //where (t,o) = model state action
  40
  41 Start = flatten
  42         [ ["pPlusAssociative: ":test pPlusAssociative]
  43         , ["pPlusCommutative: ":test pPlusCommutative]
  44         , ["pPlusIdentity: ":test pPlusIdentity]
  45         , ["pNegSub: ":test pNegSub]
  46         , ["pNegNegId: ":test pNegNegId]
  47 //      , ["pFair: ":test pFair]
  48         ]