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
114
115
116
117
118
119
120
|
implementation module gastje
/*
Pieter Koopman, Radboud University, 2016, 2017
pieter@cs.ru.nl
Advanced programming
A simplified MBT tool based on logical properties
*/
import StdEnv, StdGeneric, GenEq
test :: p -> [String] | prop p
test p = check 1000 (holds p prop0)
check :: Int [Prop] -> [String]
check n [] = ["Proof\n"]
check 0 l = ["Passed\n"]
check n [p:x]
| p.bool = check (n-1) x
| otherwise = ["Fail for: ":reverse ["\n":p.info]]
class prop a where holds :: a Prop -> [Prop]
instance prop Bool where holds b p = [{p & bool = b}]
instance prop (a->b) | prop b & testArg a
where
holds f p = diagonal [holds (f a) {p & info = [" ",string{|*|} a:p.info]} \\ a <- gen{|*|}]
class testArg a | gen{|*|}, string{|*|}, gEq{|*|} a
:: Prop =
{ bool :: Bool
, info :: [String]
}
prop0 = {bool = True, info = []}
generic gen a :: [a]
gen{|Int|} = [0,1,-1,maxint,minint,maxint-1,minint+1:[j\\i<-[2..], j<-[i,~i]]]
gen{|Bool|} = [True,False]
gen{|Char|} = [' '..'~'] ++ ['\t\n\b']
gen{|UNIT|} = [UNIT]
gen{|PAIR|} f g = map (uncurry PAIR) (diag2 f g)
gen{|EITHER|} f g = merge (map RIGHT g) (map LEFT f)
where
merge [a:x] ys = [a: merge ys x]
merge [] ys = ys
gen{|CONS|} f = map CONS f
gen{|OBJECT|} f = map OBJECT f
gen{|RECORD|} f = map RECORD f
gen{|FIELD|} f = map FIELD f
generic string a :: a -> String
string{|Int|} i = toString i
string{|Bool|} b = toString b
string{|Char|} c = toString ['\'',c,'\'']
string{|UNIT|} _ = ""
string{|PAIR|} f g (PAIR x y) = f x + " " + g y
string{|EITHER|} f g (LEFT x) = f x
string{|EITHER|} f g (RIGHT y) = g y
string{|CONS of gcd|} f (CONS x)
| gcd.gcd_arity > 0 = "(" + gcd.gcd_name + " " + f x + ")"
| otherwise = gcd.gcd_name
string{|OBJECT|} f (OBJECT x) = f x
string{|RECORD of grd|} f (RECORD x) = "{" + grd.grd_name + "|" + f x + "}"
string{|FIELD of gfd|} f (FIELD x) = gfd.gfd_name + "=" + f x + if last "" ","
where
last = gfd.gfd_index == length gfd.gfd_cons.grd_fields - 1
maxint :: Int
maxint =: IF_INT_64_OR_32 (2^63-1) (2^31-1) //2147483647
minint :: Int
minint =: IF_INT_64_OR_32 (2^63) (2^31) //-2147483648
instance + String where + s t = s +++ t
diagonal :: [[a]] -> [a]
diagonal list = f 1 2 list []
where
f n m [] [] = []
f 0 m xs ys = f m (m+1) (rev ys xs) []
f n m [] ys = f m (m+1) (rev ys []) []
f n m [[x:r]:xs] ys = [x: f (n-1) m xs [r:ys]]
f n m [[]:xs] ys = f (n-1) m xs ys
rev [] accu = accu
rev [x:r] accu = rev r [x:accu]
/**
* TODO: mixing deep and shallow embedding. This is not how this is supposed to
* be done. These can be plain functions or classes.
*/
:: Property
= E.p t: (For) infix 0 (t -> p) [t] & prop p & string{|*|} t
| E.p: (==>) infix 0 Bool p & prop p
| E.t: (=.=) infix 4 t t & ==, string{|*|} t
instance prop Property
where
holds (f For xs) p = diagonal [holds (f x) {p & info=[string{|*|} x:p.info]} \\ x <- xs]
holds (True ==> t) p = holds t p
holds (False ==> _) p = []
holds (x =.= y) p = [{bool=x==y, info=[string{|*|} y," <> ",string{|*|} x,"; ":p.info]}]
Start =
[ ["pUpper: ":test (pUpper For ['a'..'z'])]
, ["pUpper lower: ":test (\c -> isLower c ==> pUpper c)]
, ["pFac: ":test (\i -> abs i < 10 ==> prod [1..i] =.= fac i)]
]
where
pUpper :: Char -> Bool
pUpper c = c <> toUpper c
// This fails for 0; should be <=. If we fix that, the test does not
// terminate, as there are no 1000 integers with abs i < 10.
fac :: Int -> Int
fac n
| n < 0 = 1
| otherwise = n * fac (n-1)
|
