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
------------------------------------------------------------------------
--- This library defines some auxiliaries to check contracts
--- based on specifications or pre- and postconditions provided
--- in a Curry module.
--- The interface might probably change with the further
--- development of the contract implementation.
---
--- @author Michael Hanus
--- @version November 2023
------------------------------------------------------------------------

module Test.Contract
  ( withContract1, withContract2
  , withContract1ND, withContract2ND
  , withPreContract1, withPreContract2
  , withPostContract0, withPostContract1, withPostContract2
  , withPostContract0ND, withPostContract1ND, withPostContract2ND
  )  where

import Control.Search.SetFunctions
import System.IO.Unsafe     ( trace )

---------------------------------------------------------------------------
-- Report the result of checking the pre/postconditions.
-- The first argument is a tag (the name of the operation).
-- The second argument is unified with () (used by enforceable constraints).
-- The third argument is a Boolean result that must not be False for
-- a satisfied condition.
-- The fourth argument is a string describing the context (arguments,result).

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

-- print some lines of output on stderr with flushing after each line
traceLines :: [String] -> a -> a
traceLines ls x = trace (unlines ls) x

-- show operation used to show argument or result terms to the user:
-- Currently, we use Prelude.show but this has the risk that it suspends
-- or loops.
showATerm :: Show a => a -> String
showATerm = show -- or Unsafe.showAnyTerm                 -- 

---------------------------------------------------------------------------
-- Combinators for checking of contracts having pre- and postconditions

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

---------------------------------------------------------------------------
-- Combinators for checking contracts without postconditions:

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

---------------------------------------------------------------------------
-- Combinators for checking contracts without preconditions:

-- Add postcondition contract to 0-ary operation:
withPostContract0 :: Show a => String -> (a -> Bool) -> (a -> a) -> a -> a
withPostContract0 fname postcond postobserve val
  | checkPost fname (postcond val) (unwords [showATerm (postobserve val)])
  = val

-- Add postcondition contract to 0-ary operation:
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

---------------------------------------------------------------------------