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

Last change on this file since 28520 was 28520, checked in by juergen, 7 years ago

dbc docu

File size: 17.9 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
305hygienic, keys ()
306
307<enscript highlight=scheme>
308
309(command-contract ((old new query) ....) (pat pre post) ....)
310  (lambda-list? pat)
311  (contract? result)
312
313</enscript>
314
315==== contract
316
317<macro>(contract (result ....) (pat pre post) ....)</macro>
318
319hygienic, keys ()
320
321<enscript highlight=scheme>
322
323(contract (result ....) (pat pre post) ....)
324  (lambda-list? pat)
325  (contract? result)
326
327</enscript>
328
329==== contract-arguments
330
331<procedure>(contract-arguments cnd)</procedure>
332
333function (result)
334
335<enscript highlight=scheme>
336
337(contract-arguments cnd)
338  (contract-condition? cnd)
339  (list? result)
340
341</enscript>
342
343==== contract-check-level
344
345<parameter>(or (contract-check-level) (contract-check-level x))</parameter>
346
347(or (result) ((old new (lambda (x) (contract-check-level)))))
348
349<enscript highlight=scheme>
350
351(contract-check-level)
352  (and (integer? result)
353       (<= 0 result 2)
354       "0: no checks, 1: preconditions checked, 2: pre- and postconditions checked")
355
356(contract-check-level x)
357  (and (integer? x) (<= 0 x 2))
358  (= new x)
359
360</enscript>
361
362==== contract-condition-handler
363
364<procedure>(contract-condition-handler exn)</procedure>
365
366function (result)
367
368<enscript highlight=scheme>
369
370(contract-condition-handler exn)
371  (condition? exn)
372  "result of handled exeption"
373
374</enscript>
375
376==== contract-condition?
377
378<procedure>(contract-condition? xpr)</procedure>
379
380function (result)
381
382<enscript highlight=scheme>
383
384(contract-condition? xpr)
385  #t
386  (boolean? result)
387
388</enscript>
389
390==== contract-location
391
392<procedure>(contract-location cnd)</procedure>
393
394function (result)
395
396<enscript highlight=scheme>
397
398(contract-location cnd)
399  (contract-condition? cnd)
400  (symbol? result)
401
402</enscript>
403
404==== contract-text
405
406<procedure>(contract-text cnd)</procedure>
407
408function (result)
409
410<enscript highlight=scheme>
411
412(contract-text cnd)
413  (contract-condition? cnd)
414  (string? result)
415
416</enscript>
417
418==== contract?
419
420<procedure>(contract? xpr)</procedure>
421
422function (result)
423
424<enscript highlight=scheme>
425
426(contract? xpr)
427  #t
428  (boolean? result)
429
430</enscript>
431
432==== define-macro-with-contract
433
434<macro>(define-macro-with-contract name contr (transformer-type proc))</macro>
435
436hygienic, keys ()
437
438<enscript highlight=scheme>
439
440(define-macro-with-contract name contr (transformer-type proc))
441  (contract? contr)
442  (begin
443    (push-contract! (car (contr (quote name))))
444    (define-syntax name
445      (transformer-type ((cdr (contr (quote name))) proc))))
446
447</enscript>
448
449==== define-with-contract
450
451<macro>(define-with-contract name contr proc)</macro>
452
453hygienic, keys ()
454
455<enscript highlight=scheme>
456
457(define-with-contract name contr proc)
458  (contract? contr)
459  (begin
460    (push-contract! (car (contr (quote name))))
461    (define name ((cdr (contr (quote name))) proc)))
462
463</enscript>
464
465==== exit-dbc-with
466
467<macro>(exit-dbc-with name)</macro>
468
469hygienic, keys ()
470
471<enscript highlight=scheme>
472
473(exit-dbc-with name)
474  (symbol? name)
475  "saves *contracts* in dispatcher name"
476
477</enscript>
478
479==== init-dbc
480
481<macro>(init-dbc)</macro>
482
483not hygienic, exports *contracts*, keys ()
484
485<enscript highlight=scheme>
486
487(init-dbc)
488  #t
489  "initializes exception handler"
490
491</enscript>
492
493==== lambda-list?
494
495<procedure>(lambda-list? xpr)</procedure>
496
497function (result)
498
499<enscript highlight=scheme>
500
501(lambda-list? xpr)
502  #t
503  (boolean? result)
504
505</enscript>
506
507==== macro-contract
508
509<macro>(macro-contract hyg ... (key ...) (pat fender matcher) ....)</macro>
510
511hygienic, keys ()
512
513<enscript highlight=scheme>
514
515(macro-contract hyg ... (key ...) (pat fender matcher) ....)
516  (and (nested-lambda-list? pat) (procedure? matcher))
517  (contract? result)
518
519</enscript>
520
521==== make-contract-condition
522
523<procedure>(make-contract-condition location text . arguments)</procedure>
524
525function (result)
526
527<enscript highlight=scheme>
528
529(make-contract-condition location text . arguments)
530  (and (symbol? location) (string? text))
531  (condition? result)
532
533</enscript>
534
535==== make-dispatcher
536
537<procedure>(make-dispatcher alist)</procedure>
538
539function (result)
540
541<enscript highlight=scheme>
542
543(make-dispatcher alist)
544  ((list-of? list?) alist)
545  (procedure? result)
546
547</enscript>
548
549==== matches?
550
551<macro>(matches? pat . fenders)</macro>
552
553hygienic, keys ()
554
555<enscript highlight=scheme>
556
557(matches? pat . fenders)
558  (nested-lambda-list? pat)
559  "procedure returning #t if its argument matches pat with fenders"
560
561</enscript>
562
563==== nested-lambda-list?
564
565<procedure>(nested-lambda-list? xpr)</procedure>
566
567function (result)
568
569<enscript highlight=scheme>
570
571(nested-lambda-list? xpr)
572  #t
573  (boolean? result)
574
575</enscript>
576
577==== push-contract!
578
579<macro>(push-contract! contract-docu)</macro>
580
581hygienic, keys ()
582
583<enscript highlight=scheme>
584
585(push-contract! contract-docu)
586  "documentation of a contract"
587  (matches? (set! *contracts* (cons contract-docu *contracts*)))
588
589</enscript>
590
591==== string-repeat
592
593<procedure>(string-repeat str n)</procedure>
594
595function (result)
596
597<enscript highlight=scheme>
598
599(string-repeat str n)
600  (and (string? str) (not (negative? n)))
601  (string? result)
602
603</enscript>
604
605== Author
606
607[[/users/juergen-lorenz|Juergen Lorenz]]
608
609== Last update
610
611Feb 09, 2013
612
613== License
614
615 Copyright (c) 2013, Juergen Lorenz
616 All rights reserved.
617
618Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
619
620Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
621
622Redistributions 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.
623
624THIS 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.
625
626== Version History
627; 1.0.2 : document-contracts changed again, run-tests used
628; 1.0.1 : document-contracts changed
629; 1.0 : initial import
Note: See TracBrowser for help on using the repository browser.