source: project/wiki/eggref/5/simple-contracts @ 37485

Last change on this file since 37485 was 37485, checked in by juergen, 18 months ago
File size: 10.0 KB
Line 
1[[tags: egg]]
2[[toc:]]
3
4
5== Design by contract for procedures
6
7This is my third attempt to implement Bertrand Meyer's Design by
8contract in Chicken. The other two, contracts and dbc are now considered
9obsolete.
10
11We enhance arguments and return values of lambda-expressions by pre- and
12postconditions respectively, thus marking a clear distinction between
13the duties of suppliers and clients. If the arguments of a procedure
14call pass the preconditions and a result-exception is raised, then the
15supplier is to blame. On the other hand, if a argument-exception is raised
16when a procedure-call is issued, then the client has violenced its
17duties and the supplier is not even forced to do anything at all. In
18other words, the supplier can safely assume a procedure is called
19with correct arguments, he or she need not and should not check tehem
20again.
21
22Off course, pre- and postconditions must be stored in the procedure
23itself and a representation of them must be exportable, so that both
24parties of the contract know their duties.
25
26Here is the syntax of xdefine, a macro to implement queries, i.e.
27routines without state changes. Two of the four versions are shown
28below, the first with exported documentation and fixed argument list,
29the second without documentation and variable argument list.
30Note that the documentations, post and pre, are placed next to their
31corresponding checks.
32
33<enscript highlight=scheme>
34(xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... ) xpr ....)
35(xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
36</enscript>
37
38Here name is the name of the procedure, post and pre the documentation
39of post- and preconditions,  r ... are return values with corresponding
40postconditions r? ..., a ... are argument variables with preconditions
41a? ... , as is the variable collecting rest arguments with
42preconditions as? ... for each such argument and xpr starts the body.
43
44For state-changing routines, so called commands, mostly defined on top
45of a let, xlambda must be used. The syntax for a fixed resp. variable
46argument list is
47
48<enscript highlight=scheme>
49(xlambda ((r r? ...) .. <- (a a? ...) ...) xpr ....)
50(xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ....)
51</enscript>
52
53where <- separates the return values from the arguments. The other
54symbols have the same meaning as in xdefine above.
55
56xlambda expressions return three values, the procedure itself, contract
57checked or not, depending on the value of the contract-check-level
58parameter, the precondition- and the postcondition-documentation in this
59order.
60
61In previous versions of the library, instead of <-, you had to supply
62the number of return values, either explicitly or implicitly, meaning
63one. This is still working but deprecated and will propably be removed
64in future versions.
65 
66Note, that even state changing routines must return values, at best the
67values of state variables after and before a state change has taken
68place. This makes postcondition checks and command chaining easy.
69
70=== Documentation
71
72==== simple-contracts
73
74<procedure>(simple-contracts sym ..)</procedure>
75
76documentation procedure. Shows the exported symbols and the syntax of
77such an exported symbol, respectively.
78
79==== contract-check-level
80
81<parameter>(contract-check-level n ..)</parameter>
82
83no contract checks if n is -1
84only precondition checks if n is 0, the default
85pre- and postcondition checks if n is +1
86
87==== xdefine
88
89<macro>(xdefine ((r r? ...) .. name (a a? ...) ... ) xpr ....)</macro>
90<macro>(xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... ) xpr ....)</macro>
91<macro>(xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)</macro>
92<macro>(xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... as as?  ...) xpr ....)</macro>
93
94Contract guarded version of define for procedures, where
95name is the name of the procedure,
96post and pre document post- and preconditions
97r ... are return values with corresponding postconditions r? ...
98a ... are arguments with preconditions a? ...
99as is a variable collecting rest-parameters with preconditions as? for
100each such argument,
101and xpr starts the body..
102
103==== xlambda
104
105<macro>(xlambda ((r r? ...) .. <- (a a? ...) ...) xpr ....)</macro>
106<macro>(xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ....)</macro>
107
108where <- separates the results r with postconditions r? ... from the
109arguments a with preconditions a? ... a rest-parameter as with
110preconditions as? for each such argument and the body xpr .....
111
112Each xlambda call returns three values, the procedure proper,
113contract-checked or not, depending on the value of contract-check-level, and
114documentation of pre- and postconditions in this order.
115
116Deprecated versions of xlambda exist as well. Here k is the number of
117returned values, if provided, one otherwise.
118
119<macro>(xlambda k ((r r? ...) ... (a a? ...) ... ) xpr ....)</macro>
120<macro>(xlambda k ((r r? ...) ... (a a? ...) ... as as? ...) xpr ....)</macro>
121<macro>(xlambda ((r r? ...) (a a? ...) ... ) xpr ....)</macro>
122<macro>(xlambda ((r r? ...) (a a? ...) ... as as? ...) xpr ....)</macro>
123
124procedures with state change should return the values of state variables
125after and before the state change.
126
127==== %%
128
129<procedure>(%% proc)</procedure>
130
131multi argument version of flip, which can be used in pipe
132
133==== pipe
134
135<macro>(pipe combination ...)</macro>
136
137sequencing curried combinations from left to right
138
139=== Requirements
140
141checks, simple-exceptions
142
143=== Examples
144
145<enscript highlight=scheme>
146
147(import simple-contracts simple-exceptions)
148
149(define-values (counter! counter)
150  (let ((state 0))
151    (values
152      (xlambda ((new (pipe (= (add1 old))))
153                     ;integer? (pipe (= (add1 old))))
154                     ;integer? (lambda (x) (= x (add1 old))))
155                (old integer?)
156                <-) ; no arguments
157        (let ((old state))
158          (set! state (add1 state))
159          (values state old)))
160      (xlambda ((result (pipe (= state)))
161                <-) ; no arguments
162        state))))
163(counter) ; -> 0
164(counter!)
165(counter)  ; -> 1
166(counter!)
167(counter)  ; -> 2
168
169(define-values (push pop top)
170  (let ((stk '()))
171    (let (
172      (push
173        (xlambda ((new list? (pipe (equal? (cons arg old))))
174                  (old list?)
175                  <-
176                  (arg))
177          (let ((old stk))
178            (set! stk (cons arg stk))
179            (values stk old))))
180      (pop
181        (xlambda ((new list? (pipe (equal? (cdr old))))
182                  (old list?)
183                  <-)
184          (let ((old (<< stk 'pop (pipe (null?) (not)))))
185            (set! stk (cdr stk))
186            (values stk old))))
187      (top
188        (xlambda ((result) <-)
189          (car (<< stk 'top (pipe (null?) (not))))))
190      )
191      (values push pop top)
192      )))
193;(top) ; precondition violated
194;(pop) ; precondition violated
195(push 0)
196(push 1)
197(top) ; -> 1
198(call-with-values (lambda () (push 2)) list) ; -> '((2 1 0) (1 0))
199(top) ; -> 2
200(call-with-values (lambda () (pop)) list) ; -> '((1 0) (2 1 0))
201
202(define-values (add add-pre add-post)
203  (xlambda ((result integer? odd? (pipe (= (apply + x y ys))))
204            <-
205            (x integer? odd?) (y integer? even?) ys integer? even?)
206    (apply + x y ys)))
207(add 1 2 4 6) ; -> 13
208(condition-case (add 1 2 3) ((exn arguments) #f)) ; -> #f
209add-pre ; -> '((x (conjoin integer? odd?))
210               (y (conjoin integer? even?))
211               ys (conjoin integer?  even?))
212add-post
213 ; -> '(result (conjoin integer? odd? (pipe (= (apply + x y ys)))))
214
215(define wrong-add
216  (xlambda ((result integer? even?)
217            <-
218            (x integer? odd?) xs integer?  even?)
219    (apply + x xs)))
220(condition-case (wrong-add 1 2 4) ((exn results) #f)) ; -> #f
221
222(define-values (divide divide-pre divide-post)
223  (xlambda ((q integer?)
224            (r (pipe (+ (* n q))
225                     (= m)))
226            <-
227            (m integer? (pipe (>= 0)))
228            (n integer? positive?))
229    (let loop ((q 0) (r m))
230      (if (< r n)
231        (values q r)
232        (loop (+ q 1) (- r n))))))
233  (call-with-values
234    (lambda () (divide 385 25))
235    list) ;-> '(15 10)
236divide-pre ; -> '((m (conjoin integer? (pipe (>= 0))))
237                  (n (conjoin integer? positive?)))
238divide-post ; -> '((q integer?)
239                   (r (pipe (+ (* n q)) (= m))))
240 
241
242(xdefine ((result integer?) #(sum-post sum sum-pre) (a integer?) as integer?)
243  (apply + a as))
244(sum 1 2 3) ; -> 6
245(condition-case (sum 1 2 #f) ((exn arguments) #f)) ; -> #f
246
247(xdefine ((result list?) wrong-sum (a integer?) as integer?)
248  (apply + a as))
249(condition-case (wrong-sum 1 2 3) ((exn results) #f)) ; -> #f
250
251</enscript>
252
253== Last update
254
255Mar 27, 2019
256
257== Author
258
259[[/users/juergen-lorenz|Juergen Lorenz]]
260
261== License
262
263 Copyright (c) 2011-2019, Juergen Lorenz
264 All rights reserved.
265
266 Redistribution and use in source and binary forms, with or without
267 modification, are permitted provided that the following conditions are
268 met:
269 
270 Redistributions of source code must retain the above copyright
271 notice, this list of conditions and the following disclaimer.
272 
273 Redistributions in binary form must reproduce the above copyright
274 notice, this list of conditions and the following disclaimer in the
275 documentation and/or other materials provided with the distribution.
276 Neither the name of the author nor the names of its contributors may be
277 used to endorse or promote products derived from this software without
278 specific prior written permission.
279   
280 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
281 IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
282 TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
283 PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
284 HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
285 SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
286 TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
287 PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
288 LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
289 NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
290 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
291
292== Version History
293; 1.0 : port from chicken-4
Note: See TracBrowser for help on using the repository browser.