source: project/wiki/design-by-contract @ 28112

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

design-by-contract

File size: 11.4 KB
Line 
1[[toc:]]
2
3== Design by Contract
4
5Design by Contract is a programming paradigm invented by Bertrand Meyer
6for his purely Object Oriented Language Eiffel. The objective is to
7reduce the complexity of software by means of a clear separation of
8concerns between its suppliers and clients. One of the rules is: Never
9do a check an both sides of the abstraction barrier. To achieve this,
10Eiffel fosters a style, in which each routine clearly specifies, what
11are the assumptions (preconditions) of a routine and what are its
12propositions (postconditions). Moreover, the runtime system is able to
13check these conditions. If now a routine call fails because of illegal
14arguments, the client is to blame, but if it fails with violated
15propositions, it is the supplier's fault. The routine's body will not
16even be accessed with violated assumptions , and the routine will not
17even return with violated propositions.
18
19The metaphor is that of a contract between supplier and client. The
20supplier guarantees correct results, provided the client fulfills his
21duties. If not, the supplier is not obligated to start work at all. As
22in real life, both parties need a copy of the contract, and there must
23be a judge in case of troubles. Translated to programming, this means,
24the contract needs to be documented, and both parties can trust each
25other, so that they need not - and should not - check the other's
26duties, the runtime system will do it. It's a bit like proving a
27mathematical theorem: to prove its proposition, the assumptions can be
28taken for granted. Without them, the proposition is simply meaningless.
29
30== Command-query-separation
31
32There is still another metaphor of Meyer's, Command-Query-Separation.
33That means, that the programmer should never write routines both for a
34result and for a side-effect (like the ++ operators in C). Instead, two
35routines should be written, one that returns a result, the other that
36changes state. The former are called queries by Meyer, the latter
37commands (because all of Eiffel's routines operate on objects, they
38either query or command its state). In Scheme we have functions without
39side-effect, written for their results only (the recommended style), and
40state-changing procedures, which are normally denoted with a trailing
41bang. But independent of the different terminology, the principle
42applies to Scheme as well, in fact to every language.
43
44Design by Contract is such a powerful paradigm, that anybody, who ever
45has programmed in Eiffel, would like to have it in his favorite
46language. Outside the Lisp family of languages, you where out of luck,
47but Lisps, being programmable programming languages, allow you to add
48to the language what you miss. In Lisp, you are a language designer as
49well as a programmer! In what follows, you'll see, how easy it is to
50implement Design by Contract in Chicken Scheme.
51
52== The dbc module
53
54This egg is an attempt, to bring DbC to Chicken Scheme. A module written
55in this style - let's call it "example" in this turorial - has to import
56dbc. Its body should be enclosed in
57
58<enscript highlight="scheme">
59(init-dbc)
60...
61(exit-dbc-with example)
62</enscript>
63
64which guarantees, that documentation is automatically collected and
65saved in a dipatcher routine, by convention the module's name. Calling
66the dispatcher with no arguments returns a list of the exported symbols,
67with one of these symbols, it returns the symbol's documentation and
68called with a string it saves the skeleton of wiki-documentation in a
69file with the string's name.
70
71This automatic documentation is essential for DbC, after all a contract
72without a treaty, i.e. the "small print" is useless, since both parties
73need to know and accept their rights and duties.
74
75=== The syntax
76
77Let's start with the interface. We'll package the needed macros and
78procedures into a Chicken module called dbc. The fundamental macros are
79called
80
81* contract (for functions),
82* command-contract (for commands) and
83* macro-contract (for low-level macros).
84
85Their syntax is similar to the syntax of syntax-rules as explained
86below.
87
88There are no contracts for high-level macros, because the pattern
89matching process of syntax-rules can be considered as precondition
90checking. After all, macros are evaluated at compile time, i.e. before
91runtime. Hence they have no access to an expression's value, they treat
92expressions as literal lists.  Hence preconditions can only check, if
93those expressions match some patterns .... But something should be done
94to document the accepted patterns, since syntax-rules' error messages
95
96  during expansion of (name ...) - no rule matches form: (name ...)
97
98don't help without documentation:
99
100* push-contract!
101
102can provide the necessary documentation by hand.
103
104These contract macros are used with
105
106<enscript highlight="scheme">
107(define-with-contract contract-expression procedure)
108</enscript>
109
110for both procedure types and
111
112<enscript highlight="scheme">
113(define-macro-with-contract
114   macro-contract-expression
115   macro-transformer-expression).
116</enscript>
117
118Above I said, that the syntax of contract expressions is similar to the
119syntax of syntax-rules
120
121<enscript highlight="scheme">
122(syntax-rules (key ...) (pat0 tpl0) (pat1 tpl1) ...)
123</enscript>
124
125where pat0, pat1 ... are nested lambda-lists and tpl0, tpl1, ... the
126templates to be generated by the macro for the first pattern matching
127the macro's use.
128
129==== Macro contracts
130
131A macro-contract expression changes the templates to matchers, i.e.
132routines which check, if the macro expansion matches some nested
133lambda-list and eventually some additional conditions. The matches?
134macro will do that job.  Moreover, the patterns pat0, pat1 ... must
135eventually pass some fenders to be considered a match (this is an
136extension well known from syntax-case macros of R6RS). And last, but
137not least, low-level macros might be unhygienic, and the "dirty"
138symbols which pollute the name-space should be documented. In sum,
139macro-contracts look like this, if we use pseudo-variables .. and ....
140(besides ellipses, ..., "repeat the pattern on the left zero or many
141times") to mean "repeat the pattern to the left zero or one times, or
142one or many times" respectively.
143
144<enscript highlight="scheme">
145(macro-contract hyg ... (key ...) (pat fender matcher) ....)
146</enscript>
147
148==== Function contracts
149
150Functions without side effect are controlled by
151
152<enscript highlight="scheme">
153(contract (result ....) (pat pre post) ....)
154</enscript>
155
156where pat is now a lambda-list, pre a precondition and post a
157postcondition, pre an expression checking the pattern variables of pat,
158and post checking the results. Note that pre might refer to the pattern
159variables of pat and post additionally to result .... Since strings and
160symbols always return #t, you can use them as pre- or postconditions.
161
162==== Command contracts
163
164Commands, i.e. procedures without return values, which change some
165state variables instead, require the most complex contract. We need to
166check, which state variables are changed and how. Now, commands are
167usually accompanied by queries, which are functions operating on a
168subset of the command's arguments and returning state. For example,
169to set-car! corresponds car, which might be used to control what
170set-car! changes. In sum, command-contract looks as follows
171
172<enscript highlight="scheme">
173(command-contract ((old new query) ....) (pat pre post) ....)
174</enscript>
175
176where now post operates on the pattern variables of pat as well as the
177old and new variables. But here remains one twist: The macro can't
178know, on which subset of the command's arguments the queries operate.
179We must tell it. In other words, the supplied queries must be lifted to
180command's argument list.
181
182Note that despite their similarities, there is one difference in the
183postconditions of these three contract macros: procedure contracts
184require an expression, while macro-contract requires a predicate, i.e.
185a function.
186
187==== A first example
188
189Let's consider an example, a function with two return values, Euclid's
190integer division. Note that this contract proves, that the function
191does what it is supposed to do!
192
193<enscript highlight="scheme">
194(define-with-contract q+r
195  (contract (q r) ; two results
196    ((_ m n)
197     (and ; preconditions
198      (integer? m) (not (negative? m))
199      (integer? n) (positive? n)
200      (<= n m))
201     (and ; postconditions
202       (integer? q)
203       (integer? r)
204       (= (+ (* q n) r) m))))
205  (lambda (m n)
206    (let loop ((q 0) (r m))
207      (if (< r n)
208        (values q r)
209        (loop (+ q 1) (- r n))))))
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 a module-global
220variable *contracts*, supplied by init-dbc (which must therefore be
221unhygienic), and apply the contract's checker to its procedure argument.
222
223Isn't that a lot of checking code, you might ask, and you are right.
224Therefor there is a parameter,
225
226* contract-check-level
227
228with values 0, 1 and 2, meaning "no checks at all, only documentation",
229"check only preconditions" or "check everything" respectively. The
230default is 1, but in the developing phase you'll probably set it to 2.
231
232==== How to organize your code?
233
234Typically, you'll place the raw definitions without any defenses in one
235module, say raw-foo, and import their names with a prefix into another
236one, say foo, to add the contracts to them. These prefixed names can
237than be used in foo's contracts as well. The second module, foo, is
238the one to be exported.
239
240The splitting into two modules has several advantages.
241First, it helps developing. Usually, you'll have an idea, what a
242routine should do and how to implement it. At this stage, you needn't
243bother about "defensing programming" or anything like this, you can add
244the defenses later. You can already test your ideas incrementally and
245see if they do what they are supposed to do.
246
247Second, you wouldn't like to check these defenses again and again in
248your own routines, in particular in recursive ones. It's better to do
249the checks only once from outside.
250
251Third, you can enhance your old modules with contracts later on
252without touching the code.
253
254Fourth, if you like driving without a security belt and are concerned
255with speed, you can import raw-foo instead of foo into client code.
256
257==== Another example with two modules
258
259The following rather contrieved example may clarify this. The resulting
260module, foo, contains all three contract types.
261
262<enscript highlight="scheme">
263(module raw-foo (adder adder! freeze)
264        (import scheme)
265
266        (define state 0)
267        (define (adder) state)
268        (define (adder! n) (set! state (+ state n)))
269        (define (freeze form inject compare?)
270                `(lambda () ,(cadr form)))
271) ; end raw-foo
272</enscript>
273
274Then you define and add the contracts to the prefixed names
275
276<enscript highlight="scheme">
277
278(require-library dbc)
279
280(module foo (adder adder! freeze)
281        (import (prefix (except raw-foo freeze) "%"))
282        (import-for-syntax (prefix (only raw-foo freeze) "%"))
283
284        (define-with-contract adder
285                (contract (result)
286                        ((_) #t (number? result)))
287                %adder)
288
289        (define-with-contract adder!
290                (command-contract ((old new (lambda (n) (%adder))))
291                        ((_ n) (number? n) (= new (+ old n))))
292                %adder!)
293
294        (define-macro-with-contract freeze
295                (macro-contract () ((_ x) #t (matches? (lambda () x))))
296                (ir-macro-transformer %freeze))
297) ; end foo
298</enscript>
299
300== Author
301
302[[/users/juergen-lorenz|Juergen Lorenz]]
303
304== Initial version
305
306Jan 15, 2013
307
Note: See TracBrowser for help on using the repository browser.