files/practicum/StdQTest.icl

   1 module StdQTest
   2
   3 /*      Test module StdQTest
   4         Voor werken met Gast:
   5                 (*) gebruik Environment 'Gast'
   6                 (*) zet Project Options op 'Basic Values Only'
   7 */
   8
   9 import StdQ
  10 import StdEnv
  11 import gast
  12
  13 Start
  14                 = testn 1000
  15                         (\ a b c ->
  16                            let qa = fromInt a
  17                        in  zero_is_neutral_for_addition      qa /\
  18                                zero_is_neutral_for_subtraction   qa /\
  19                                one_is_neutral_for_multiplication qa /\
  20                                one_is_neutral_for_division       qa /\
  21                                negation_is_idempotent            qa /\
  22                                add_then_subtract_yields_identity qa /\
  23                                subtract_then_add_yields_identity qa /\
  24                                abs_is_positive                   qa /\
  25                                isInt_holds_for_Ints              qa /\
  26                                toQ_yields_rational            a b c /\
  27                                True
  28                         )
  29
  30 zero_is_neutral_for_addition            :: Q -> Property
  31 zero_is_neutral_for_addition a          = name "zero_is_neutral_for_addition"
  32                                                                                (zero + a == a && a == a + zero)
  33
  34 zero_is_neutral_for_subtraction         :: Q -> Property
  35 zero_is_neutral_for_subtraction a       = name "zero_is_neutral_for_subtraction"
  36                                                                                (a - zero == a && a == ~ (zero - a))
  37
  38 one_is_neutral_for_multiplication       :: Q -> Property
  39 one_is_neutral_for_multiplication a     = name "one_is_neutral_for_multiplication"
  40                                                                                (one * a == a && a == a * one)
  41
  42 zero_is_zero_for_multiplication         :: Q -> Property
  43 zero_is_zero_for_multiplication a       = name "zero_is_zero_for_multiplication"
  44                                                                                (zero * a == zero && zero == a * zero)
  45
  46 one_is_neutral_for_division                     :: Q -> Property
  47 one_is_neutral_for_division a           = name "one_is_neutral_for_division"
  48                                                                                (a / one == a)
  49
  50 negation_is_idempotent                          :: Q -> Property
  51 negation_is_idempotent a                        = name "negation_is_idempotent"
  52                                                                                (~ (~ a) == a)
  53
  54 add_then_subtract_yields_identity       :: Q -> Property
  55 add_then_subtract_yields_identity a     = name "add then subtract" ((a + a) - a == a)
  56
  57 subtract_then_add_yields_identity       :: Q -> Property
  58 subtract_then_add_yields_identity a     = name "subtract then add" ((zero - a - a) + a + a == zero)
  59
  60 abs_is_positive                     :: Q -> Property
  61 abs_is_positive a                   = name "abs is positive" (abs a >= zero)
  62
  63 isInt_holds_for_Ints                            :: Q -> Property
  64 isInt_holds_for_Ints a                          = name "isInt holds for Ints" (isInt a && (a == zero || not (isInt (a / (a+a)))))
  65
  66 toQ_yields_rational                                     :: Int Int Int -> Property
  67 toQ_yields_rational a b c                       = name "toQ yields rational"
  68                                                                                ( (abs a > 2^30 || abs b > 2^30 || a*b == zero || toQ (a,b) * toQ b == toQ a)
  69                                                                                  &&
  70                                                                                  (abs a > 2^30 || abs b > 2^30 || abs c > 2^30 || a*b*c == zero || (toQ (c,a,b) - toQ c) * toQ b == toQ a)
  71                                                                                )
  72
  73 instance fromInt Q where fromInt i      = toQ i