source: project/wiki/design-by-contract-old-version @ 35656

Last change on this file since 35656 was 31126, checked in by Mario Domenech Goulart, 6 years ago

Properly capitalize CHICKEN on the wiki directory (only first level).

I used the following shell script to change things:

while IFS= read -d $'\0' -r file ; do

sed -i 's/Chicken/CHICKEN/g' "$file"

done < <(find wiki -maxdepth 1 -type f -print0 )

Some files have been manually reverted after that, since some
substitutions don't apply:

  • friedly-chicken (repl banner)
  • survey2011 (Chicken in URI paths)
  • chickenista-guide (Chickenista)

I hope the link canonicalization thing will be on my side.

File size: 9.4 KB
Line 
1[[toc:]]
2
3== Design by Contract
4
5Design by Contract - DbC for short - is a metaphor introduced by Bertrand Meyer for its purely object-oriented language Eiffel. The idea consists in strictly separating the concerns of clients and suppliers of code. The supplier of a routine is not obliged to check the validity of its arguments, that's the clients duty. And in fact the supplier mustn't do it to avoid double checks. On the other hand, the supplier has to guarantee correct results of his or her routine, the client can rely on it. It's like a contract between two parties. But like a contract in social life, the "small-print" is part of the contract, hence this software contract must be documented automatically, so that each party knows each-others duties and benefits.
6
7== Command-query-separation
8
9Another idea of Meyer's is command-query-separation, where he names a function without side-effect a "query" (it returns part of the state of his objects) and a procedure without returned value acting by side-effect only a "command" (it changes the state of his objects). His suggestion is never to do both in one routine (like the ++ operators in C), write two instead. This is a suggestion only, it can not be enforced.
10
11== The contracts module
12
13This egg is an attempt, to bring DbC to CHICKEN Scheme. A module written in this style - let's call it "example" in this turorial - has to import contracts. Its body should be enclosed in
14
15<enscript highlight="scheme">
16(doclist '())
17...
18(define example (doclist->dispatcher (doclist)))
19</enscript>
20
21where doclist is a paramter, to generate automatic documentation. This documentation can be accessed by the client in two ways. First by calling (example) without arguments, returning the list of all symbols, exported by the example module, second by calling (example 'foo) returning a representation of foo's contract provided foo is an exported symbol.
22
23Well, this contracts must be supplied, before their representations can be exported. This is done by replacing define and define-syntax in the module body with define-with-contract and define-syntax-with-contract. And of course, these latter macros must contain the actual contracts in some way.
24
25== The case of procedures
26
27The contracts module supplies a short and a long form of define-with-syntax, where the short form looks like this
28
29<enscript highlight="scheme">
30(define-with-contract (foo . args) clause ... . body)
31</enscript>
32
33where each clause is either a docstring or one of the following expressions
34
35<enscript highlight="scheme">
36(domain: assumption ...)
37(range: proposition ...) or (range: (with-results (name ...) proposition ...))
38(effect: (state query change [equ?]) ...)
39</enscript>
40
41The assumption ... expressions check the assumptions (including the types) of the arguments args, the proposition ... expressions the result-names name ... (without with-results the one result name "result" is assumed) and the (state query change)  triples the change of the variable state initialized with the query expression before the command call to its value after the command call. Comparison is done with equal? [or equ?, if that argument is supplied]. Note, that the effect: triples are similar to the triples in the declaration part of do.
42
43Note that command-query-separation demands, that at most one of a range: and an effect: clause is supplied.
44
45The long form of define-with-contract looks like this
46
47<enscript highlight="scheme">
48(define-with-contract foo
49  (contract (foo . args)
50    clause
51    ...)
52  (lambda args . body))
53</enscript>
54
55where the clauses are the same as in the short form.
56
57Here is a nontrivial example, the implementation of the single datatype, which allows to encapsulate a value and change it as well.
58
59<enscript highlight="scheme">
60(use contracts)
61
62;;; initialize documentation
63(doclist '())
64
65;;; predicate
66(define-with-contract (single? xpr)
67   "check, if xpr evaluates to a single"
68   (and (procedure? xpr)
69        (condition-case (eq? 'single (xpr (lambda (a b c) a)))
70          ((exn) #f))))
71
72;;; constructor
73(define-with-contract (single xpr)
74  "package the value of xpr into a single object"
75  (domain: (true? xpr))
76  (range: (single? result))
77  (lambda (sel)
78    (sel 'single xpr (lambda (new) (set! xpr new)))))
79
80;;; query
81(define-with-contract (single-state sg)
82  "returns the state of the single object sg"
83  (domain: (single? sg))
84  (range: (true? result))
85  (sg (lambda (a b c) b)))
86
87;;; command
88(define-with-contract (single-state! sg arg)
89  "replaces state of sg with arg"
90  (domain: (single? sg) (true? arg))
91  (effect: (state (single-state sg) arg))
92  ((sg (lambda (a b c) c)) arg))
93
94;;; save documentation in a dispatcher
95(define singles (doclist->dispatcher (doclist)))
96</enscript>
97
98Here is another example, a function with two results, Euclid's integer division.
99
100<enscript highlight="scheme">
101
102(define-with-contract (quotient+remainder m n)
103  "integer division"
104  (domain:
105    (integer? m)
106    (not (negative? m))
107    (integer? n)
108    (positive? n)
109    (<= n m))
110  (range:
111    (with-results (q r)
112      (integer? q)
113      (integer? r)
114      (= (+ (* q n) r) m)))
115  (let loop ((q 0) (r m))
116    (if (< r n)
117      (values  q r)
118      (loop (add1 q) (- r n)))))
119 
120</enscript>
121
122Up to now, we have used keywords domain:, range: and effect: to implement the contracts. If you don't like them, you can use symbols domain, range and effect as well.
123
124== The case of macros
125
126It's easy for syntax-rules macros. After all, matching the macro-code against some patterns is already a domain check! Since macro transformers have only access to forms, not to runtime values, only the forms can be checked. Consequently we have to do only two things, supply a docstring for documentation and export the admissible macro-codes, which can be extracted from the patterns. In sum, checked macros are defined in example's body like this
127
128<enscript highlight="scheme">
129(define-syntax-with-contract foo
130  "docstring"
131  (syntax-rules () (code xpr) ...))
132</enscript>
133
134the only difference to define-syntax being the mandatory docstring - but the textual representations of code ... will be exported by a call to (example 'foo)!
135
136Contracts of low-level macros are harder to implement. After all we have to destructure the macro-code by hand and take care of all the renaming.  Since the macro-transformer doesn't expose admissible patterns, we either must supply and check them or we must package the destructuring and renaming into a macro with the same syntax as syntax-rules. Then we can handle it like syntax-rules. But to do this, we need other macros like destructuring-bind in Common Lisp or match in the matchable package.
137
138The contracts module will export all the necessary means to do the job, namely binding constructs, bind and bind-case (in fact, only restricted versions of them, more powerfull ones are located in the bindings module) as well as the macros ir-macro-rules and er-macro-rules which mimic syntax-rules. To use the latter two we must import them for syntax.
139
140Like in the case of functions there should be short forms of define-syntax-with-contract as well.
141
142The following examples show how a trivial freeze macro could be implemented in all these variants. If you run it, you should inspect the documentation as well by calling syntax-contracts-test with or without a symbol. And you should supply wrong macro-calls like (efreeze 1 2) to see the error messages ....
143
144<enscript highlight=scheme>
145
146(use contracts)
147(import-for-syntax
148  (only contracts er-macro-rules ir-macro-rules))
149
150(doclist '())
151
152(define-syntax-with-contract (sefreeze xpr)
153  "sefreeze"
154  (with-renamed (%lambda) `(,%lambda () ,xpr)))
155
156(define-syntax-with-contract (sifreeze xpr)
157  "sifreeze"
158  (with-injected () `(lambda () ,xpr)))
159
160(define-syntax-with-contract (ssfreeze xpr)
161  "ssfreeze"
162  (literal () (lambda () xpr)))
163
164(define-syntax-with-contract sfreeze
165  "sfreeze"
166  (syntax-rules ()
167    ((_ xpr) (lambda () xpr))))
168
169(define-syntax-with-contract ifreeze
170  "ifreeze"
171  (ir-macro-rules ()
172    ((_ xpr) `(lambda () ,xpr))))
173
174(define-syntax-with-contract efreeze
175  "efreeze"
176  (er-macro-rules (%lambda)
177    ((_ xpr) `(,%lambda () ,xpr))))
178
179(define-syntax-with-contract lifreeze
180  (syntax-contract (lifreeze xpr) "lifreeze")
181  (ir-macro-transformer
182    (lambda (f i c) `(lambda () ,(cadr f)))))
183
184(define-syntax-with-contract lefreeze
185  (syntax-contract (lefreeze xpr) "lefreeze")
186  (er-macro-transformer
187    (lambda (f r c) `(,(r 'lambda) () ,(cadr f)))))
188
189(define syntax-contracts-test (doclist->dispatcher (doclist)))
190
191</enscript>
192
193You might have noticed, that we didn't check a macro-transformer's range. That can be done but it would need another matching process. And that would be overkill. After all, we can inspect that range with an expand call.
194
195Up to now I've only noted, that the contract representations are exported for documentation.  But of course, the routine's contracts check the routine's implementation behind the scene, delivering meaningful error-messages in case of troubles.
196
197You might argue, that this is a lot of error checking. And you are right. But chicken has an interpreter besides a compiler. So the contracts module arranges the checks in such a way, that only the interpreter checks propositions and assumptions, whereas in compiled code only the latter are checked.
198
199If you are still concerned about speed of compiled code, you can compile with the unsafe switch, disabling domain checks as well. But this is like driving without a security belt ...
200
201
202== Author
203
204[[/users/juergen-lorenz|Juergen Lorenz]]
205
206== Initial version
207
208Jun 23, 2011
209
210== Updated
211
212Sep 14, 2011
Note: See TracBrowser for help on using the repository browser.