source: project/wiki/eggref/4/dbc @ 31105

Last change on this file since 31105 was 31105, checked in by juergen, 6 years ago

dbc version 1.0.3 docu improved

File size: 17.4 KB
Line 
1[[tags: egg]]
2[[toc:]]
3
4== dbc
5
6=== Design by Contract
7
8Design by Contract is a programming paradigm invented by Bertrand Meyer
9for his purely Object Oriented Language Eiffel. The objective is to
10reduce the complexity of software by means of a clear separation of
11concerns between its suppliers and clients. One of the rules is: Never
12do a check an both sides of the abstraction barrier. To achieve this,
13Eiffel fosters a style, in which each routine clearly specifies, what
14are the assumptions (preconditions) of a routine and what are its
15propositions (postconditions). Moreover, the runtime system is able to
16check these conditions. If now a routine call fails because of illegal
17arguments, the client is to blame, but if it fails with violated
18propositions, it is the supplier's fault. The routine's body will not
19even be accessed with violated assumptions , and the routine will not
20even return with violated propositions.
21
22The metaphor is that of a contract between supplier and client. The
23supplier guarantees correct results, provided the client fulfills his
24duties. If not, the supplier is not obligated to start work at all. As
25in real life, both parties need a copy of the contract, and there must
26be a judge in case of troubles. Translated to programming, this means,
27the contract needs to be documented, and both parties can trust each
28other, so that they need not - and should not - check the other's
29duties, the runtime system will do it. It's a bit like proving a
30mathematical theorem: to prove its proposition, the assumptions can be
31taken for granted. Without them, the proposition is simply meaningless.
32
33There is still another metaphor of Meyer's, Command-Query-Separation.
34That means, that the programmer should never write routines both for a
35result and for a side-effect (like the ++ operators in C). Instead, two
36routines should be written, one that returns a result, the other that
37changes state. The former are called queries by Meyer, the latter
38commands (because all of Eiffel's routines operate on objects, they
39either query or command its state). In Scheme we have functions without
40side-effect, written for their results only (the recommended style), and
41state-changing procedures, which are normally denoted with a trailing
42bang. But independent of the different terminology, the principle
43applies to Scheme as well, in fact to every language.
44
45Design by Contract is such a powerful paradigm, that anybody, who ever
46has programmed in Eiffel, would like to have it in his favorite
47language. Outside the Lisp family of languages, you where out of luck,
48but Lisps, being programmable programming languages, allow you to add
49to the language what you miss. In Lisp, you are a language designer as
50well as a programmer! In what follows, you'll see, how easy it is to
51implement Design by Contract in Chicken Scheme.
52
53=== The syntax
54
55Let's start with the interface. We'll package the needed macros and
56procedures into a Chicken module called dbc. The fundamental macros are
57called
58
59* contract (for functions),
60* command-contract (for commands) and
61* macro-contract (for low-level macros).
62
63Their syntax is similar to the syntax of syntax-rules as explained
64below.
65
66There are no contracts for high-level macros, because the pattern
67matching process of syntax-rules can be considered as precondition
68checking. After all, macros are evaluated at compile time, i.e. before
69runtime. Hence they have no access to an expression's value, they treat
70expressions as literal lists.  Hence preconditions can only check, if
71those expressions match some patterns .... But something should be done
72to document the accepted patterns, since syntax-rules' error messages
73
74  during expansion of (name ...) - no rule matches form: (name ...)
75
76don't help without documentation:
77
78* push-contract!
79
80can provide the necessary documentation by hand.
81
82These contract macros are used with
83
84<enscript highlight=scheme>
85
86  (define-with-contract contract-expression procedure)
87
88</enscript>
89
90for both procedure types and
91
92<enscript highlight=scheme>
93
94  (define-macro-with-contract
95    macro-contract-expression
96    macro-transformer-expression).
97
98</enscript>
99
100All these macro calls must be enclosed into two other macro calls,
101(init-dbc) and (exit-dbc-with name). The first macro is unhygienic,
102because its call will define a global variable, *contracts*, to collect
103the documentation of contracts, and it will initialize a special
104exception-handler. The second macro call will store the collected
105documentation in a dispatcher, name, by convention the module name. The
106call (name) will then list the documented symbols, (name 'sym) the
107documentation of sym and (name "file") will store the whole
108documentation in file in a wiki like format.
109
110Note that automatic documentation is essential for design by contract.
111After all, a contract without a contract document, the "small print" is
112useless.
113
114Above I said, that the syntax of contract expressions is similar to the
115syntax of syntax-rules
116
117<enscript highlight=scheme>
118
119  (syntax-rules (key ...) (pat0 tpl0) (pat1 tpl1) ...)
120
121</enscript>
122
123where pat0, pat1 ... are nested lambda-lists and tpl0, tpl1, ... the
124templates to be generated by the macro for the first pattern matching
125the macro's use.
126
127A macro-contract expression changes the templates to matchers, i.e.
128routines which check, if the macro expansion matches some nested
129lambda-list and eventually some additional conditions. The matches?
130macro will do that job.  Moreover, the patterns pat0, pat1 ... must
131eventually pass some fenders to be considered a match (this is an
132extension well known from syntax-case macros of R6RS). And last, but
133not least, low-level macros might be unhygienic, and the "dirty"
134symbols which pollute the name-space should be documented. In sum,
135macro-contracts look like this, if we use pseudo-variables .. and ....
136(besides ellipses, ..., "repeat the pattern on the left zero or many
137times") to mean "repeat the pattern to the left zero or one times, or
138one or many times" respectively.
139
140<enscript highlight=scheme>
141
142  (macro-contract hyg ... (key ...) (pat fender matcher) ....)
143
144</enscript>
145
146Functions without side effect are controlled by
147
148<enscript highlight=scheme>
149
150  (contract (result ....) (pat pre post) ....)
151
152</enscript>
153
154where pat is now a lambda-list, pre a precondition and post a
155postcondition, pre an expression checking the pattern variables of pat,
156and post checking the results. Note that pre might refer to the pattern
157variables of pat and post additionally to result .... Since strings and
158symbols always return #t, you can use them as pre- or postconditions.
159
160Commands, i.e. procedures without return values, which change some
161state variables instead, require the most complex contract. We need to
162check, which state variables are changed and how. Now, commands are
163usually accompanied by queries, which are functions operating on a
164subset of the command's arguments and returning state. For example,
165to set-car! corresponds car, which might be used to control what
166set-car! changes. In sum, command-contract looks as follows
167
168<enscript highlight=scheme>
169
170  (command-contract ((old new query) ....) (pat pre post) ....)
171
172</enscript>
173
174where now post operates on the pattern variables of pat as well as the
175old and new variables. But here remains one twist: The macro can't
176know, on which subset of the command's arguments the queries operate.
177We must tell it. In other words, the supplied queries must be lifted to
178command's argument list.
179
180Note that despite their similarities, there is one difference in the
181postconditions of these three contract macros: procedure contracts
182require an expression, while macro-contract requires a predicate, i.e.
183a function.
184
185=== Example
186
187Let's consider an example, a function with two return values, Euclid's
188integer division. Note that this contract proves, that the function
189does what it is supposed to do!
190
191<enscript highlight=scheme>
192
193  (define-with-contract q+r
194    (contract (q r) ; two results
195      ((_ m n)
196       (and ; preconditions
197        (integer? m) (not (negative? m))
198        (integer? n) (positive? n)
199        (<= n m))
200       (and ; postconditions
201         (integer? q)
202         (integer? r)
203         (= (+ (* q n) r) m))))
204    (lambda (m n)
205      (let loop ((q 0) (r m))
206        (if (< r n)
207          (values q r)
208          (loop (+ q 1) (- r n))))))
209
210</enscript>
211
212=== How do all these macros work?
213
214Well, it's relatively simple. The three contract expressions return a
215pair, consisting of its own documentation and a procedure. The latter
216does the actual checks. In other words, it accepts another procedure as
217argument and returns that very procedure with annotated checks.
218
219The two defines store the contract's documentation in *contracts*,
220supplied by init-dbc, and apply the contract's checker to its procedure
221argument.
222
223Isn't that a lot of checking code, you might ask, and you are right.
224Therefor there is a parameter, contract-check-level, with values 0, 1
225and 2, meaning "no checks at all, only documentation", "check only
226preconditions" or "check everything" respectively. The default is 1,
227but in the developing phase you'll probably set it to 2.
228
229=== How to organize your code?
230
231Typically, you'll place the raw definitions without any defenses in one
232module, say %foo, and import their names with a prefix into another
233one, say foo, to add the contracts to them. These prefixed names can
234than be used in foo's contracts as well. The second module, foo, is
235the one to be exported.
236
237Off course, you can work the other way as well: Write the interface
238module with the contracts first, using prefixed names for the routines
239to be implemented in and imported from the raw implementation module.
240This is the official code development strategy.
241
242The splitting into two modules has several advantages.
243First, it helps developing. Usually, you'll have an idea, what a
244routine should do and how to implement it. At this stage, you needn't
245bother about "defensing programming" or anything like this, you can add
246the defenses later. You can already test your ideas incrementally and
247see if they do what they are supposed to do.
248
249Second, you wouldn't like to check these defenses again and again in
250your own routines, in particular in recursive ones. It's better to do
251the checks only once from outside.
252
253Third, you can enhance your old modules with contracts later
254without touching the code.
255
256Fourth, if you like driving without a security belt and are concerned
257with speed, you can import %foo instead of foo into client code.
258
259=== Another example
260
261The following rather contrieved example may clarify this. The resulting
262module, foo, contains all three contract types.
263
264<enscript highlight=scheme>
265
266  (module %foo (adder adder! freeze)
267  (import scheme)
268  (define state 0)
269  (define (adder) state)
270  (define (adder! n) (set! state (+ state n)))
271  (define (freeze form inject compare?)
272    `(lambda () ,(cadr form)))
273  ) ; end %foo
274
275</enscript>
276
277Then you define and add the contracts to the prefixed names
278
279<enscript highlight=scheme>
280
281  (module foo (adder adder! freeze)
282  (import (prefix (except %foo freeze) "%"))
283  (import-for-syntax (prefix (only %foo freeze) "%"))
284  (define-with-contract adder
285    (contract (result)
286      ((_) #t (number? result)))
287    %adder)
288  (define-with-contract adder!
289    (command-contract ((old new (lambda (n) (%adder))))
290      ((_ n) (number? n) (= new (+ old n))))
291    %adder!)
292  (define-macro-with-contract freeze
293    (macro-contract () ((_ x) #t (matches? (lambda () x))))
294    (ir-macro-transformer %freeze))
295  ) ; end foo
296
297</enscript>
298
299=== Exported routines
300
301==== command-contract
302
303<macro>(command-contract ((old new query) ....) (pat pre post) ....)</macro>
304
305<enscript highlight=scheme>
306hygienic, keys ()
307requires (lambda-list? pat)
308ensures  (contract? result)
309</enscript>
310
311==== contract
312
313<macro>(contract (result ....) (pat pre post) ....)</macro>
314
315<enscript highlight=scheme>
316hygienic, keys ()
317requires (lambda-list? pat)
318ensures  (contract? result)
319</enscript>
320
321==== contract-arguments
322
323<procedure>(contract-arguments cnd)</procedure>
324
325<enscript highlight=scheme>
326function (result)
327requires (contract-condition? cnd)
328ensures  (list? result)
329</enscript>
330
331==== contract-check-level
332
333<parameter>(contract-check-level x ..)</parameter>
334
335<enscript highlight=scheme>
336requires (and (integer? x)
337              (<= 0 x 2)
338              "0: no checks"
339              "1: preconditions checked"
340              "2: pre- and postconditions checked")
341</enscript>
342
343==== contract-condition-handler
344
345<procedure>(contract-condition-handler exn)</procedure>
346
347<enscript highlight=scheme>
348function (result)
349requires (condition? exn)
350ensures  result of handled exeption
351</enscript>
352
353==== contract-condition?
354
355<procedure>(contract-condition? xpr)</procedure>
356
357<enscript highlight=scheme>
358function (result)
359requires #t
360ensures  (boolean? result)
361</enscript>
362
363==== contract-location
364
365<procedure>(contract-location cnd)</procedure>
366
367<enscript highlight=scheme>
368function (result)
369requires (contract-condition? cnd)
370ensures  (symbol? result)
371</enscript>
372
373==== contract-text
374
375<procedure>(contract-text cnd)</procedure>
376
377<enscript highlight=scheme>
378function (result)
379requires (contract-condition? cnd)
380ensures  (string? result)
381</enscript>
382
383==== contract?
384
385<procedure>(contract? xpr)</procedure>
386
387<enscript highlight=scheme>
388function (result)
389requires #t
390ensures  (boolean? result)
391</enscript>
392
393==== define-macro-with-contract
394
395<macro>(define-macro-with-contract name contr (transformer-type proc))</macro>
396
397<enscript highlight=scheme>
398hygienic, keys ()
399requires (contract? contr)
400ensures  (begin (push-contract! (car (contr (quote name)))) (define-syntax name (transformer-type ((cdr (contr (quote name))) proc))))
401</enscript>
402
403==== define-with-contract
404
405<macro>(define-with-contract name contr proc)</macro>
406
407<enscript highlight=scheme>
408hygienic, keys ()
409requires (contract? contr)
410ensures  (begin (push-contract! (car (contr (quote name)))) (define name ((cdr (contr (quote name))) proc)))
411</enscript>
412
413==== exit-dbc-with
414
415<macro>(exit-dbc-with name)</macro>
416
417<enscript highlight=scheme>
418hygienic, keys ()
419requires (symbol? name)
420ensures  saves *contracts* in dispatcher name
421</enscript>
422
423==== init-dbc
424
425<macro>(init-dbc)</macro>
426
427<enscript highlight=scheme>
428unhygienic, exports *contracts* keys ()
429requires #t
430ensures  initializes exception handler
431</enscript>
432
433==== lambda-list?
434
435<procedure>(lambda-list? xpr)</procedure>
436
437<enscript highlight=scheme>
438function (result)
439requires #t
440ensures  (boolean? result)
441</enscript>
442
443==== macro-contract
444
445<macro>(macro-contract hyg ... (key ...) (pat fender matcher) ....)</macro>
446
447<enscript highlight=scheme>
448hygienic, keys ()
449requires (and (nested-lambda-list? pat) (procedure? matcher))
450ensures  (contract? result)
451</enscript>
452
453==== make-contract-condition
454
455<procedure>(make-contract-condition location text . arguments)</procedure>
456
457<enscript highlight=scheme>
458function (result)
459requires (and (symbol? location) (string? text))
460ensures  (condition? result)
461</enscript>
462
463==== make-dispatcher
464
465<procedure>(make-dispatcher alist)</procedure>
466
467<enscript highlight=scheme>
468function (result)
469requires ((list-of? list?) alist)
470ensures  (procedure? result)
471</enscript>
472
473==== matches?
474
475<macro>(matches? pat . fenders)</macro>
476
477<enscript highlight=scheme>
478hygienic, keys ()
479requires (nested-lambda-list? pat)
480ensures  procedure returning #t if its argument matches pat with fenders
481</enscript>
482
483==== nested-lambda-list?
484
485<procedure>(nested-lambda-list? xpr)</procedure>
486
487<enscript highlight=scheme>
488function (result)
489requires #t
490ensures  (boolean? result)
491</enscript>
492
493==== push-contract!
494
495<macro>(push-contract! contract-docu)</macro>
496
497<enscript highlight=scheme>
498hygienic, keys ()
499requires documentation of a contract
500ensures  (matches? (set! *contracts* (cons contract-docu *contracts*)))
501</enscript>
502
503==== string-repeat
504
505<procedure>(string-repeat str n)</procedure>
506
507<enscript highlight=scheme>
508function (result)
509requires (and (string? str) (not (negative? n)))
510ensures  (string? result)
511</enscript>
512
513== Author
514
515[[/users/juergen-lorenz|Juergen Lorenz]]
516
517== Last update
518
519Jul 08, 2014
520
521== License
522
523 Copyright (c) 2013, Juergen Lorenz
524 All rights reserved.
525
526Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
527
528Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
529
530Redistributions 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.
531
532THIS 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.
533
534== Version History
535; 1.0.3 : document-contracts changed
536; 1.0.2 : document-contracts changed again, run-tests used
537; 1.0.1 : document-contracts changed
538; 1.0 : initial import
Note: See TracBrowser for help on using the repository browser.