1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
implementation module cashModel
/*
Pieter Koopman, Radboud University, 2017
pieter@cs.ru.nl
Advanced programming
A simple state model for an automated cash register
*/
import StdEnv, GenEq
import gastje
from Data.Func import mapSt
import Data.Tuple
class euro a :: a -> Euro
instance euro Product
where
euro Pizza = euro (4,99)
euro Beer = euro (0,65)
euro _ = euro 1
instance euro Int where euro e = {euro = e, cent = 0}
instance euro (Int, Int) where euro (e,c) = {euro = e, cent = c}
instance euro [e] | euro e where euro l = sum (map euro l)
instance euro Euro where euro e = e
instance + Euro
where
+ x y = {euro = c / 100, cent = (abs c) rem 100}
where
c = (x.euro + y.euro) * 100 + sign x.euro * x.cent + sign y.euro * y.cent
instance - Euro
where
- x y = {euro = c / 100, cent = (abs c) rem 100}
where
c = (x.euro - y.euro) * 100 + sign x.euro * x.cent - sign y.euro * y.cent
instance zero Euro where zero = {euro = 0, cent = 0}
derive gEq Euro, Product
instance == Product where (==) p q = p === q
instance == Euro where (==) p q = p === q
instance ~ Euro where ~ e = {e & euro = ~e.euro}
model :: [Product] Action -> ([Product],[Euro])
model list (Add p) = ([p:list],[euro p])
model list (Rem p)
| isMember p list = (removeMember p list,[~ (euro p)])
| otherwise = (list,[])
model list Pay = ([],[euro list])
derive gEq Action
derive gen Euro, Action, Product, []
derive string Euro, Action, Product, []
derive bimap []
/**
* plus_zero_is_identity: Fail for: {Euro|euro=0, cent=1} ; {Euro|euro=0, cent=1} <> {Euro|euro=0, cent=0}
* plus_is_commutative: Passed
* minus_zero_is_identity: Fail for: {Euro|euro=0, cent=1} ; {Euro|euro=0, cent=1} <> {Euro|euro=0, cent=0}
* prop_double_neg_is_identity: Passed
* prop_neg_is_not_identity: Fail for: {Euro|euro=0, cent=1}
* prop_minus_is_plus_after_neg: Fail for: {Euro|euro=1, cent=0} {Euro|euro=-9223372036854775808, cent=1} ; {Euro|euro=0, cent=99} <> {Euro|euro=1, cent=1}
* prop_neg_distributes_over_plus: Fail for: {Euro|euro=1, cent=0} {Euro|euro=-9223372036854775808, cent=1} ; {Euro|euro=-1, cent=1} <> {Euro|euro=0, cent=99}
* prop_plus_minus_is_identity: Fail for: {Euro|euro=0, cent=1} {Euro|euro=0, cent=0} ; {Euro|euro=0, cent=0} <> {Euro|euro=0, cent=1}
*/
Start =
[ ["plus_zero_is_identity: ": test prop_plus_zero_is_identity]
, ["plus_is_commutative: ": test prop_plus_is_commutative]
, ["minus_zero_is_identity: ": test prop_minus_zero_is_identity]
, ["prop_double_neg_is_identity: ": test prop_double_neg_is_identity]
, ["prop_neg_is_not_identity: ": test prop_neg_is_not_identity]
, ["prop_minus_is_plus_after_neg: ": test prop_minus_is_plus_after_neg]
, ["prop_neg_distributes_over_plus: ": test prop_neg_distributes_over_plus]
, ["prop_plus_minus_is_identity: ": test prop_plus_minus_is_identity]
]
where
prop_plus_zero_is_identity :: Euro -> Property
prop_plus_zero_is_identity e = e + zero =.= e
prop_plus_is_commutative :: Euro Euro -> Property
prop_plus_is_commutative a b = a + b =.= b + a
prop_minus_zero_is_identity :: Euro -> Property
prop_minus_zero_is_identity e = e - zero =.= e
prop_plus_minus_is_identity :: Euro Euro -> Property
prop_plus_minus_is_identity a b = a =.= a - b + b
prop_double_neg_is_identity :: Euro -> Property
prop_double_neg_is_identity e = ~(~e) =.= e
prop_neg_is_not_identity :: Euro -> Property
prop_neg_is_not_identity e = e <> zero ==> e <> ~e
prop_minus_is_plus_after_neg :: Euro Euro -> Property
prop_minus_is_plus_after_neg a b = a - b =.= a + ~b
prop_neg_distributes_over_plus :: Euro Euro -> Property
prop_neg_distributes_over_plus a b = ~(a + b) =.= ~a + ~b
/**
* Passed
*
* NB: this only checks Rem (as requested). The same property holds for Add.
* For Pay, the output of the model should be negated.
*/
Start = test fairness
where
fairness :: [Product] Product -> Property
fairness ps p = euro newps =.= euro ps + euro out
where (newps, out) = model ps (Rem p)
|
