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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
module Test.Contract
( withContract1, withContract2
, withContract1ND, withContract2ND
, withPreContract1, withPreContract2
, withPostContract0, withPostContract1, withPostContract2
, withPostContract0ND, withPostContract1ND, withPostContract2ND
) where
import Control.SetFunctions
import System.IO.Unsafe ( trace )
checkPre :: String -> Bool -> String -> Bool
checkPre fname result arg = case result of
True -> True
False -> traceLines
["Precondition of "++fname++" violated for:",arg]
(error "Execution aborted due to contract violation!")
checkPreND :: String -> Values Bool -> String -> Bool
checkPreND fname result arg = case False `valueOf` result of
True -> traceLines
["Precondition of "++fname++" violated for:",arg]
(error "Execution aborted due to contract violation!")
False -> True
checkPost :: String -> Bool -> String -> Bool
checkPost fname result arg = case result of
True -> True
False -> traceLines
["Postcondition of "++fname++" violated "++
"for:", arg]
(error "Execution aborted due to contract violation!")
checkPostND :: String -> Values Bool -> String -> Bool
checkPostND fname result arg = case False `valueOf` result of
True -> traceLines
["Postcondition of "++fname++" violated "++
"for:", arg]
(error "Execution aborted due to contract violation!")
False -> True
traceLines :: [String] -> a -> a
traceLines ls x = trace (unlines ls) x
showATerm :: Show a => a -> String
showATerm = show
withContract1 :: (Show a, Show b) => String
-> (a -> Bool) -> (a -> b -> Bool) -> (b -> b)
-> (a -> b) -> a -> b
withContract1 fname precond postcond postobserve fun arg
| checkPre fname (precond arg) (showATerm arg)
&> checkPost fname (postcond arg result)
(unwords [showATerm arg, "->", showATerm (postobserve result)])
= result
where result = fun arg
withContract1ND :: (Show a, Show b) => String
-> (a -> Values Bool) -> (a -> b -> Values Bool) -> (b -> b)
-> (a -> b) -> a -> b
withContract1ND fname precond postcond postobserve fun arg
| checkPreND fname (precond arg) (showATerm arg)
&> checkPostND fname (postcond arg result)
(unwords [showATerm arg, "->", showATerm (postobserve result)])
= result
where result = fun arg
withContract2 :: (Show a, Show b, Show c) => String
-> (a -> b -> Bool) -> (a -> b -> c -> Bool)
-> (c -> c) -> (a -> b -> c) -> a -> b -> c
withContract2 fname precond postcond postobserve fun arg1 arg2
| checkPre fname (precond arg1 arg2)
(unwords [showATerm arg1,showATerm arg2])
&> checkPost fname (postcond arg1 arg2 result)
(unwords [showATerm arg1, showATerm arg2, "->",
showATerm (postobserve result)])
= result
where result = fun arg1 arg2
withContract2ND :: (Show a, Show b, Show c) => String
-> (a -> b -> Values Bool) -> (a -> b -> c -> Values Bool)
-> (c -> c) -> (a -> b -> c) -> a -> b -> c
withContract2ND fname precond postcond postobserve fun arg1 arg2
| checkPreND fname (precond arg1 arg2)
(unwords [showATerm arg1,showATerm arg2])
&> checkPostND fname (postcond arg1 arg2 result)
(unwords [showATerm arg1, showATerm arg2, "->",
showATerm (postobserve result)])
= result
where result = fun arg1 arg2
withPreContract1 :: Show a => String -> (a -> Bool) -> (a -> b) -> a -> b
withPreContract1 fname precond fun arg
| checkPre fname (precond arg) (showATerm arg)
= fun arg
withPreContract2 :: (Show a, Show b) => String -> (a -> b -> Bool)
-> (a -> b -> c) -> a -> b -> c
withPreContract2 fname precond fun arg1 arg2
| checkPre fname (precond arg1 arg2)
(unwords [showATerm arg1,showATerm arg2])
= fun arg1 arg2
withPostContract0 :: Show a => String -> (a -> Bool) -> (a -> a) -> a -> a
withPostContract0 fname postcond postobserve val
| checkPost fname (postcond val) (unwords [showATerm (postobserve val)])
= val
withPostContract0ND :: Show a => String -> (a -> Values Bool) -> (a -> a) -> a -> a
withPostContract0ND fname postcond postobserve val
| checkPostND fname (postcond val) (unwords [showATerm (postobserve val)])
= val
withPostContract1 :: (Show a, Show b) => String -> (a -> b -> Bool) -> (b -> b)
-> (a -> b) -> a -> b
withPostContract1 fname postcond postobserve fun arg
| checkPost fname (postcond arg result)
(unwords [showATerm arg, "->", showATerm (postobserve result)])
= result
where result = fun arg
withPostContract1ND :: (Show a, Show b) => String
-> (a -> b -> Values Bool) -> (b -> b)
-> (a -> b) -> a -> b
withPostContract1ND fname postcond postobserve fun arg
| checkPostND fname (postcond arg result)
(unwords [showATerm arg, "->", showATerm (postobserve result)])
= result
where result = fun arg
withPostContract2 :: (Show a, Show b, Show c) =>
String -> (a -> b -> c -> Bool) -> (c -> c)
-> (a -> b -> c) -> a -> b -> c
withPostContract2 fname postcond postobserve fun arg1 arg2
| checkPost fname (postcond arg1 arg2 result)
(unwords [showATerm arg1, showATerm arg2, "->",
showATerm (postobserve result)])
= result
where result = fun arg1 arg2
withPostContract2ND :: (Show a, Show b, Show c) =>
String -> (a -> b -> c -> Values Bool) -> (c -> c)
-> (a -> b -> c) -> a -> b -> c
withPostContract2ND fname postcond postobserve fun arg1 arg2
| checkPostND fname (postcond arg1 arg2 result)
(unwords [showATerm arg1, showATerm arg2, "->",
showATerm (postobserve result)])
= result
where result = fun arg1 arg2
|