source: project/wiki/eggref/4/contracts @ 26738

Last change on this file since 26738 was 26738, checked in by juergen, 9 years ago

contracts: internal macro check-em: message argument in assert now string

File size: 15.6 KB
Line 
1[[tags: egg]]
2[[toc:]]
3
4== contracts
5
6=== Design by Contract
7
8"Design by contract" is a metaphor coined by Bertrand Meyer for his purely object oriented language Eiffel. The idea behind it is to separate the concerns of suppliers and clients of software modules: The client of a routine is responsible for calling it with correct arguments. The supplier can rely on it, she/he mustn't check it again.  The supplier in turn is responsible for delivering correct results, provided the routine's arguments are valid. If not, the supplier needn't do any work at all.
9
10In this metaphor a module is something like a contract between the supplier and the client of that module. But like a contract in social life, it's useless if not properly documented. Hence the "small print" of our module should be documented automatically, so that each party knows about each others duties ....
11
12=== Command-query-separation
13
14Another metaphor of Meyer's is "command-query-separation", where in Eiffel a command is working by side effect (it changes the object's state) and a query is a pure function (it reports the object's state without changing it). His advice is, never to do both in one routine, write two instead.
15
16=== Implementation and use
17
18This module is an attempt to bring Design by Contract to Chicken Scheme.  In effect, it replaces define and define-syntax by new macros define-with-contract and define-syntax-with-contract respectively, where - in the long form - the lambda or syntax-rules expression is preceeded by a contract expression. A short form is available as well, where the call pattern of the procedure is followed by the contract clauses and the procedure's body.
19
20To achieve automatic documentation, these two macros have to be wrapped by a call of the parameter
21
22<enscript highlight=scheme>(doclist '())</enscript>
23
24initializing documentation and the definition
25
26<enscript highlight=scheme>(define module-name (doclist->dispatcher (doclist)))</enscript>
27
28saving it in a dispatcher routine.
29
30==== The case of procedures
31
32For procedures a contract expression starts with the symbol contract and contains a list of clauses, where each clause is either
33
34* the pattern of a typical procedure's call, the only required clause,
35
36* a documentation string,
37
38* a list starting with the keyword domain: (or the literal domain) and containing checks of the assumptions,
39
40* a list starting with the keyword range: (or the literal range) followed either by (with-results (result0 result1 ...) xpr0 xpr1 ...) or by xpr0 xpr1 ..., where xpr0 xpr1 are predicates on result0 result1 ... or the default variable name result.
41
42* a list starting with the keyword effect: (or the literal effect) which contains triples of the form (state query change [equ?]) where state is bound to the query expression before the command call and the change expression is compared with equal? [or equ?, if supplied] to another call of query after the command call.
43
44Note, that command-query-separation demands, that only one of a range: and an effect: clause are allowed.
45
46==== The case of macros
47
48For syntax-rules macros as well as ir-macro-rules and er-macro-rules macros the contract expression is simply a docstring. After all, those macro-transformers have domain checks already built-in in form of the pattern matching process, it needs only be automatically documented.
49
50For raw low-level macros based on (er-|ir-)macro-transformer, it's a list starting with the macro code (name . rest) which will be matched against the macro's use and an optional documentation string.
51
52=== Programming interface of module contract-helpers
53
54==== contract-helpers
55
56<procedure>(contract-helpers [sym])</procedure>
57
58prints the contract of the exported symbol sym of the contract-helpers module or the list of exported symbols when called as a thunk.
59
60==== er-macro-rules
61
62<syntax>(er-macro-rules (%sym ...) (code0 xpr0) (code1 xpr1) ...)</syntax>
63
64references a renamed version of sym ... under the name %sym ... and pairs the differnt macro-codes code0 code1 ... with expressions xpr0 xpr1 ..., which usually evalute to backquoted templates.
65
66This macro is unhygienic by design, it introduces the symbol compare? into its scope.
67
68==== ir-macro-rules
69
70<syntax>(ir-macro-rules (sym ...) (code0 xpr0) (code1 xpr1) ...)</syntax>
71
72pairs the differnt macro-codes code0 code1 ... with expressions xpr0 xpr1 ..., which usually evalute to backquoted templates in the scope of injected symbols sym ....
73
74This macro is unhygienic by design, it introduces the two symbols inject and compare? into its scope.
75
76==== bind
77
78<syntax>(bind pat xpr . body)</syntax>
79
80binds the pattern variables of the nested lambda-list pat to corresponding subexpressions of the nested pseudolist xpr and executes body in this context.
81
82==== bind-case
83
84<syntax>(bind-case xpr (pat0 . body0) (pat1 . body1) ...)</syntax>
85
86matches nested pseudolist-expression xpr against patterns pat0 pat1 ...  in sequence, binding the variables of the first matching pattern to corresponding subexpressions of xpr and executes body of the first matching pattern in this context.
87
88==== doclist
89
90<parameter>(doclist '())</parameter>
91
92should be called before the first define[-syntax]-with-contract expression to initialize automatic documentation.
93
94==== doclist->dispatcher
95
96<procedure>(doclist->dispatcher (doclist))</procedure>
97
98saves (doclist) in a dispatcher. A typical use is
99
100<enscript highlight=scheme>
101(define module-name (doclist->dispatcher (doclist)))
102</enscript>
103
104which should be called after the last define[-syntax]-with-contract expression to save the automatic documentation in module-name. This procedure can than be called by the module's client with or without a symbol argument.
105
106<enscript highlight=scheme>
107(module-name [sym])
108</enscript>
109
110Without argument the  call returns the list of exported symbols, with argument the call returns the textual representaion of the contract of the module's exported symbol sym.
111
112==== print-doclist
113
114<procedure>(print-doclist)</procedure>
115
116prints the documentation of the whole module in readable form.
117
118=== Programming interface of module contracts
119
120All exported symbols of contract-helpers are passed through, so that it's only necessary to import contracts.
121
122==== contracts
123
124<procedure>(contracts [sym])</procedure>
125
126prints the contract of the exported symbol sym of the contracts module or the list of exported symbols when called as a thunk.
127
128==== contract
129
130<syntax>(contract (name . args) clause ...)</syntax>
131
132where each clause is one of
133
134* a documentation string
135
136* {{(domain: assumption ...)}}
137
138* {{(range: proposition ...) or (range: (with-results (res0 res1 ...) proposition ...)}}
139
140* {{(effect: (state query change [equ?]) ...)}}
141
142==== define-with-contract
143
144One of
145
146<syntax>(define-with-contract name (contract (name . args) clause ...) (lambda args . body))</syntax>
147
148<syntax>(define-with-contract name (let ((var val) ...) (contract (name . args) clause ...) (lambda args . body)))</syntax>
149
150<syntax>(define-with-contract (name . args) clause ... . body)</syntax>
151
152where the admissible clauses are described above and instead of let another binding construct can be used as well.
153
154==== define-syntax-with-contract
155
156One of
157
158<syntax>(define-syntax-with-contract name docstring rules)</syntax>
159
160where rules is one of
161
162* {{(syntax-rules (sym ...) (pat0 tpl0) (pat1 tpl1) ...)}}
163
164* {{(ir-macro-rules (sym ...) (pat0 xpr0) (pat1 xpr1) ...)}}
165
166* {{(er-macro-rules (%sym ...) (pat0 xpr0) (pat1 xpr1) ...)}}
167
168and docstring is optional,
169
170<syntax>(define-syntax-with-contract name (syntax-contract (name . rest) docstring) transformer)</syntax>
171
172where docstring is optional and transformer is a raw low-level macro-transformer,
173
174<syntax>(define-syntax-with-contract (name . rest) docstring with-expression)</syntax>
175
176where docstring is optional and with-expression is one of
177
178* {{(literal syms . body)}}
179
180* {{(with-renamed syms . body)}}
181
182* {{(with-injected syms . body)}}
183
184which will be translated to syntax-rules, er-macro-rules or ir-macro-rules respectively.
185
186==== define-macro-with-contract
187
188<syntax>(define-macro-with-contract code docstring body))</syntax>
189
190where docstring is optional, code is the complete macro-code (name . args), i.e. the pattern of a macro call, and body is one of
191
192  (with-renamed (%sym ...) xpr . xprs)
193  (with-injected (sym ...) xpr . xprs)
194  xpr . xprs
195
196In the first case each %sym is a renamed version of sym, in the second sym is injected as is, i.e. not renamed, and in the last case no symbol is injected, i.e. the macro is hygienic.
197
198== Usage
199
200<enscript highlight=scheme>
201(use contracts)
202(import-for-syntax
203  (only contacts er-macro-rules ir-macro-rules))
204</enscript>
205
206== Examples
207
208<enscript highlight=scheme>
209
210(use contacts)
211
212(import-for-syntax
213 (only contracts ir-macro-rules er-macro-rules))
214
215;;; initialize documentation
216(doclist '())
217
218;;; a single datatype as an alternative to boxes
219
220;; predicate
221(define-with-contract (single? xpr)
222   "check, if xpr evaluates to a single"
223   (and (procedure? xpr)
224        (condition-case (eq? 'single (xpr (lambda (a b c) a)))
225          ((exn) #f))))
226
227;; constructor
228(define-with-contract (single xpr)
229  "package the value of xpr into a single object"
230  (domain: (true? xpr))
231  (range: (single? result))
232  (lambda (sel)
233    (sel 'single xpr (lambda (new) (set! xpr new)))))
234
235;; query
236(define-with-contract (single-state sg)
237  "returns the state of the single object sg"
238  (domain: (single? sg))
239  (range: (true? result))
240  (sg (lambda (a b c) b)))
241
242;; command
243(define-with-contract (single-state! sg arg)
244  "replaces state of sg with arg"
245  (domain: (single? sg) (true? arg))
246  (effect: (state (single-state sg) arg))
247  ((sg (lambda (a b c) c)) arg))
248
249;;; Euclid's integer division as an example for a
250;;; function with two results
251
252(define-with-contract (quotient+remainder m n)
253  "integer division"
254  (domain:
255    (integer? m)
256    (not (negative? m))
257    (integer? n)
258    (positive? n)
259    (<= n m))
260  (range:
261    (with-results (q r)
262      (integer? q)
263      (integer? r)
264      (= (+ (* q n) r) m)))
265  (let loop ((q 0) (r m))
266    (if (< r n)
267      (values  q r)
268      (loop (add1 q) (- r n)))))
269 
270;;; the same trivial freeze macro implemented in different styles
271
272(define-syntax-with-contract (sefreeze xpr)
273  "sefreeze"
274  (with-renamed (%lambda) `(,%lambda () ,xpr)))
275
276(define-syntax-with-contract (sifreeze xpr)
277  "sifreeze"
278  (with-injected () `(lambda () ,xpr)))
279
280(define-syntax-with-contract (ssfreeze xpr)
281  "ssfreeze"
282  (literal () (lambda () xpr)))
283
284(define-syntax-with-contract sfreeze
285  "sfreeze"
286  (syntax-rules ()
287    ((_ xpr) (lambda () xpr))))
288
289(define-syntax-with-contract ifreeze
290  "ifreeze"
291  (ir-macro-rules ()
292    ((_ xpr) `(lambda () ,xpr))))
293
294(define-syntax-with-contract efreeze
295  "efreeze"
296  (er-macro-rules (%lambda)
297    ((_ xpr) `(,%lambda () ,xpr))))
298
299(define-syntax-with-contract lifreeze
300  (syntax-contract (lifreeze xpr) "lifreeze")
301  (ir-macro-transformer
302    (lambda (f i c) `(lambda () ,(cadr f)))))
303
304(define-syntax-with-contract lefreeze
305  (syntax-contract (lefreeze xpr) "lefreeze")
306  (er-macro-transformer
307    (lambda (f r c) `(,(r 'lambda) () ,(cadr f)))))
308
309(define-syntax-with-contract lfreeze
310  (syntax-contract (lfreeze xpr) "lfreeze")
311  (lambda (f r c) `(,(r 'lambda) () ,(cadr f))))
312
313;;; explicit- and implicit-renaming versions of or
314
315(define-syntax-with-contract er-or
316  "er-version of or"
317  (er-macro-rules (%if %er-or)
318    ((_) #f)
319    ((_ arg . args)
320     `(,%if ,arg ,arg (,%er-or ,@args)))))
321 
322(define-syntax-with-contract ir-or
323  "ir-version of or"
324  (ir-macro-rules ()
325    ((_) #f)
326    ((_ arg . args)
327     `(if ,arg ,arg (ir-or ,@args)))))
328 
329(define-macro-with-contract (our-or . args)
330  "a private version of or"
331  (if (null? args)
332    #f
333    (let ((tmp (car args)))
334      `(if ,tmp ,tmp (our-or ,@(cdr args))))))
335
336(define-macro-with-contract (my-or . args)
337  "a variant of or"
338  (with-renamed (%if %my-or)
339    (if (null? args)
340      #f
341      (let ((tmp (car args)))
342        `(,%if ,tmp ,tmp (,%my-or ,@(cdr args)))))))
343
344;; save documantation in dispatcher
345(define docs (doclist->dispatcher (doclist)))
346
347;; some binding-examples with results
348
349(bind x 1 x)  ; -> 1
350
351(bind (x (y (z . u) v) . w) '(1 (2 (3) 4) 5 6)
352        (list x y z u v w)) ; -> (1 2 3 () 4 (5 6))
353
354(bind (x (y (z . u) v) . w) '(1 (2 (3 . 3) 4) 5 6)
355        (list x y z u v w)) ; -> (1 2 3 3 4 (5 6))
356
357(bind-case '(1 (2 3))
358        ((x (y z)) (list x y z))
359        ((x (y . z)) (list x y z))
360        ((x y) (list x y))) ; -> (1 2 3)
361
362(bind-case '(1 (2 3))
363        ((x (y . z)) (list x y z))
364        ((x y) (list x y))
365        ((x (y z)) (list x y z))) ; -> (1 2 (3))
366
367(bind-case '(1 (2 3))
368        ((x y) (list x y))
369        ((x (y . z)) (list x y z))
370        ((x (y z)) (list x y z))) ; -> (1 (2 3))
371
372(bind-case '(1 (2 . 3))
373        ((x (y . z)) (list x y z))
374        ((x (y z)) (list x y z))) ; -> (1 2 3)
375
376(bind-case '(1 (2 . 3))
377        ((x y) (list x y))
378        ((x (y . z)) (list x y z))
379        ((x (y z)) (list x y z))) ; -> (1 (2 . 3))
380
381</enscript>
382
383== Author
384
385[[/users/juergen-lorenz|Juergen Lorenz]]
386
387== Initial version
388
389Jun, 2011
390
391== Updated
392
393May 18, 2012
394
395== License
396
397 Copyright (c) 2011, Juergen Lorenz
398 All rights reserved.
399
400Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
401
402Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
403
404Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.  Neither the name of the author nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
405
406THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
407
408== Version History
409
410; 2.0.4 : internal macro check-em corrected, message arguments in assert now strings
411; 2.0 : (er|ir)-macro-define-with-contract unified to define-macro-with-contract
412; 1.9 : with-aliases and matches? removed from interface, bind and bind-case rewritten
413; 1.8 : Code split into two modules, added matches? with-aliases er-macro-define-with-contract ir-macro-define-with-contract
414; 1.7 : Code fixed to work with new transformer syntax in Chicken-4.7.3, syntax-contract removed as separate macro but retained as literal symbol in define-syntax-with-contract, define-syntax-with-contract rewritten
415; 1.6 : bind and bind-case exported again: needed by ir-macros and er-macros
416; 1.5 : removed bind, bind-case rewritten but removed from interface
417; 1.4 : various chenges: removed unnecessary dependencies, removed bind-let* and matches? from interface, define-syntax-with-contract and bind rewritten, comments updated, ...
418; 1.3 : changed with-literal to literal
419; 1.2 : added bind bind-let* bind-case matches syntax-contract ir-macro-rules er-macro-rules, changed define-syntax-with-contract
420; 1.1 : (results: ...) made obsolete, use (with-results (name ...) . body) within (range: ...) instead
421; 1.0 : changed (effect: ...), removed (state: ...) (invariant: ...)
422; 0.4 : some enhancements
423; 0.3 : added {{print-doclist}}, fixed typo in setup script reported by mario
424; 0.2 : bugfixes
425; 0.1 : initial import
426
Note: See TracBrowser for help on using the repository browser.