source: project/wiki/simple-design-by-contract @ 37488

Last change on this file since 37488 was 37488, checked in by juergen, 11 months ago
File size: 6.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 another metaphor of Meyer's, Command-Query-Separation:
33the 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 anyone who has ever
45programmed in Eiffel, would like to have it in his favorite
46language. Outside the Lisp family of languages, you are out of luck,
47but Lisps, being programmable programming languages, allow you to add
48features to the language. 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 simple-contracts module
53
54This egg is my third attempt, to bring DbC to CHICKEN Scheme. It only
55considers procedures, not macros. And it assumes, that the supplier code
56helps to check postconditions in case of commands. Hence, not only
57queries but commands as well return results, namely the state before and
58after a state change. So this change can be checked.
59
60Besides the parameter contract-check-level, which sets the level to
61-1, 0, or 1 respectively and according to this level, nothing, only
62preconditions or pre- and postconditions respectively are checked,
63there are in essence two macros xdefine and xlambda. For queries,
64xdefine can be used, for commands xlambda must be used.
65
66Note, that in the former case, the procedure name or a vector with the
67name and the post- and preconditions separate results from arguments,
68in the latter case, this separation is done by the special symbol <-.
69As in C the results are to the left, the arguments to the right of this
70separator. The argument- and result-names are followed by predicates
71and parenthesized, except rest parameters, where the parentheses are
72skipped. Their predicates check each argument of the rest parameter.
73
74<enscript highlight=scheme>
75
76(xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... ) xpr ....)
77(xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
78
79</enscript>
80
81<enscript highlight=scheme>
82
83(xlambda ((r r? ...) .. <- (a a? ...) ...) xpr ....)
84(xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ....)
85
86=== Examples
87
88</enscript>
89
90<enscript highlight=scheme>
91
92(import simple-contracts checks)
93
94(define-values (counter! counter)
95  (let ((state 0))
96    (values
97      (xlambda ((new (cut = <> (add1 old)))
98                ;integer? (lambda (x) (= x (add1 old))))
99                (old integer?)
100                <-)
101        (let ((old state))
102          (set! state (add1 state))
103          (values state old)))
104      (xlambda ((result (cut = <> state))
105                <-)
106        state))))
107
108(counter) ; -> 0
109(counter!)
110(counter)  ; -> 1
111(counter!)
112(counter)  ; -> 2
113
114(define-values (push pop top)
115  (let ((stk '()))
116    (let (
117          (push
118            (xlambda ((new list? (cut equal? <> (cons arg old)))
119                      (old list?)
120                      <-
121                      (arg))
122              (let ((old stk))
123                (set! stk (cons arg stk))
124                (values stk old))))
125          (pop
126            (xlambda ((new list? (cut equal? <> (cdr old)))
127                      (old list?)
128                      <-)
129              (let ((old (<<< 'pop stk (o not null?))))
130                (set! stk (cdr stk))
131                (values stk old))))
132          (top
133            (xlambda ((result) <-)
134              (car (<<< 'top stk (o not null?)))))
135          )
136      (values push pop top)
137      )))
138
139;(top) ; precondition violated
140;(pop) ; precondition violated
141(push 0)
142(push 1)
143(top) ; -> 1
144(call-with-values (lambda () (push 2)) list) ; -> '((2 1 0) (1 0))
145(top) ; -> 2
146(call-with-values (lambda () (pop)) list) ; -> '((1 0) (2 1 0))
147
148(define-values (add add-pre add-post)
149  (xlambda ((result integer? odd? (cut = <> (apply + x y ys)))
150            <-
151            (x integer? odd?) (y integer? even?) ys integer? even?)
152    (apply + x y ys)))
153
154(define-values (divide divide-pre divide-post)
155  (xlambda ((q integer?)
156            (r (lambda (x) (= (+ x (* n q)) m)))
157            <-
158            (m integer? (cut >= <> 0))
159            (n integer? positive?))
160    (let loop ((q 0) (r m))
161      (if (< r n)
162        (values q r)
163        (loop (+ q 1) (- r n))))))
164
165(xdefine ((result integer?)
166          #(sum-post sum sum-pre)
167          (a integer?) as integer?)
168  (apply + a as))
169
170</enscript>
171
172== Author
173
174[[/users/juergen-lorenz|Juergen Lorenz]]
175
Note: See TracBrowser for help on using the repository browser.