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

Last change on this file since 37489 was 37489, checked in by juergen, 14 months ago
File size: 8.8 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=== Requirements
128
129checks
130
131=== Examples
132
133<enscript highlight=scheme>
134
135(import simple-contracts checks)
136
137(define-values (counter! counter)
138  (let ((state 0))
139    (values
140      (xlambda ((new (cut = <> (add1 old)))
141                ;integer? (lambda (x) (= x (add1 old))))
142                (old integer?)
143                <-)
144        (let ((old state))
145          (set! state (add1 state))
146          (values state old)))
147      (xlambda ((result (cut = <> state))
148                <-)
149        state))))
150
151(counter) ; -> 0
152(counter!)
153(counter)  ; -> 1
154(counter!)
155(counter)  ; -> 2
156
157(define-values (push pop top)
158  (let ((stk '()))
159    (let (
160          (push
161            (xlambda ((new list? (cut equal? <> (cons arg old)))
162                      (old list?)
163                      <-
164                      (arg))
165              (let ((old stk))
166                (set! stk (cons arg stk))
167                (values stk old))))
168          (pop
169            (xlambda ((new list? (cut equal? <> (cdr old)))
170                      (old list?)
171                      <-)
172              (let ((old (<<< 'pop stk (o not null?))))
173                (set! stk (cdr stk))
174                (values stk old))))
175          (top
176            (xlambda ((result) <-)
177              (car (<<< 'top stk (o not null?)))))
178          )
179      (values push pop top)
180      )))
181
182;(top) ; precondition violated
183;(pop) ; precondition violated
184(push 0)
185(push 1)
186(top) ; -> 1
187(call-with-values (lambda () (push 2)) list) ; -> '((2 1 0) (1 0))
188(top) ; -> 2
189(call-with-values (lambda () (pop)) list) ; -> '((1 0) (2 1 0))
190
191(define-values (add add-pre add-post)
192  (xlambda ((result integer? odd? (cut = <> (apply + x y ys)))
193            <-
194            (x integer? odd?) (y integer? even?) ys integer? even?)
195    (apply + x y ys)))
196
197(define-values (divide divide-pre divide-post)
198  (xlambda ((q integer?)
199            (r (lambda (x) (= (+ x (* n q)) m)))
200            <-
201            (m integer? (cut >= <> 0))
202            (n integer? positive?))
203    (let loop ((q 0) (r m))
204      (if (< r n)
205        (values q r)
206        (loop (+ q 1) (- r n))))))
207
208(xdefine ((result integer?)
209          #(sum-post sum sum-pre)
210          (a integer?) as integer?)
211  (apply + a as))
212
213</enscript>
214
215== Last update
216
217Mar 27, 2019
218
219== Author
220
221[[/users/juergen-lorenz|Juergen Lorenz]]
222
223== License
224
225 Copyright (c) 2011-2019, Juergen Lorenz
226 All rights reserved.
227
228 Redistribution and use in source and binary forms, with or without
229 modification, are permitted provided that the following conditions are
230 met:
231 
232 Redistributions of source code must retain the above copyright
233 notice, this list of conditions and the following disclaimer.
234 
235 Redistributions in binary form must reproduce the above copyright
236 notice, this list of conditions and the following disclaimer in the
237 documentation and/or other materials provided with the distribution.
238 Neither the name of the author nor the names of its contributors may be
239 used to endorse or promote products derived from this software without
240 specific prior written permission.
241   
242 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
243 IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
244 TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
245 PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
246 HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
247 SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
248 TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
249 PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
250 LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
251 NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
252 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
253
254== Version History
255; 1.0 : port from chicken-4
Note: See TracBrowser for help on using the repository browser.