You are looking at historical revision 24574 of this page. It may differ significantly from its current revision.
- Design by Contract
- Implementation and use
- Programming interface
- Initial version
- Version History
Design by Contract
"Design by contract" is a metaphor coined by Bertrand Meyer for his purely object oriented language Eiffel. The idea behind it is to separate the concerns of suppliers and clients of software modules: The client of a routine is responsible for calling it with correct arguments. The supplier can rely on it, she/he mustn't check it again. The supplier in turn is responsible for delivering correct results, provided the routine's arguments are valid. If not, the supplier needn't do any work at all.
In this metaphor a module is something like a contract between the supplier and the client of that module. But like a contract in social life, it's useless if not properly documented. Hence the "small print" of our module should be documented automatically, so that each party knows about each others duties ....
Another metaphor of Meyer's is "command-query-separation", where in Eiffel a command is working by side effect (it changes the object's state) and a query is a pure function (it reports the object's state without changing it). His advice is, never to do both in one routine, write two instead.
Implementation and use
This module is an attempt to bring Design by Contract to Chicken Scheme. In effect, it replaces define and define-syntax by new macros define-with-contract and define-syntax-with-contract respectively, where - in the long form - the lambda or syntax-rules expression is preceeded by a contract expression. A short form is available as well, where the call pattern of the procedure is followed by the contract clauses and the procedure's body.
To achieve automatic documentation, these two macros have to be wrapped by a call of the parameter
initializing documentation and the definition
(define module-name (doclist->dispatcher (doclist)))
saving it in a dispatcher routine.
The case of procedures
For procedures a contract expression starts with the symbol contract and contains a list of clauses, where each clause is either
- the pattern of a typical procedure's call, the only required clause,
- a documentation string,
- a list starting with the keyword domain: and containing checks of the assumptions,
- a list starting with the keyword results: containing variable names which are bound to the results of the procedure; if this list is not supplied (results: result) is assumed. This is now obsolete and should be replaced by (with-results (res0 res1 ...) . body) within the range: clause below.
- a list starting with the keyword range: followed either by (with-results (result0 result1 ...) xpr0 xpr1 ...) or by xpr0 xpr1 ..., where xpr0 xpr1 are predicates on result0 result1 ... or the default variable name result.
- a list starting with the keyword effect: which contains triples of the form (state query change [equ?]) where state is bound to the query expression before the command call and the change expression is compared with equal? [or equ?, if supplied] to another call of query after the command call.
Note, that command-query-separation demands, that only one of a range: and an effect: clause are allowed.
The case of macros
For syntax-rules macros as well as ir-macro-rules and er-macro-rules macros the contract expression is simply a docstring. After all, those macro-transformers have domain checks already built-in in form of the pattern matching process, it needs only be automatically documented.
For raw low-level macros based on (er-|ir-)macro-transformer, it's a list starting with the macro code (name . rest) which will be matched against the macro's use and an optional documentation string.
contract[syntax] (contract (name . args) clause ...)
where each clause is one of
- a documentation string
- (domain: assumption ...)
- (range: proposition ...) or (range: (with-results (res0 res1 ...) proposition ...)
- (effect: (state query change [equ?]) ...)
One of[syntax] (define-with-contract name (contract (name . args) clause ...) (lambda args . body))
[syntax] (define-with-contract name (let ((var val) ...) (contract (name . args) clause ...) (lambda args . body)))
[syntax] (define-with-contract (name . args) clause ... . body)
where the admissible clauses are described above and instead of let another binding construct can be used as well.
bind[syntax] (bind pat xpr . body)
destructures the value of the expression xpr along the pattern pat, which might be a deeply nested lambda-list, binds the pattern variables to corresponding subexpressions of xpr and evaluates body in this context.
bind-let*[syntax] (bind-let* ((pat xpr) ...) . body)
recursive sequential version of bind, equivalent to
(bind pat xpr (bind-let* (...) . body)
bind-case[syntax] (bind-case xpr (pat0 . body0) (pat1 . body1) ...)
matches the value of the expression xpr against the patterns pat0 pat1 ... in sequence and executes the body paired with the first matching pattern.
matches?[syntax] (matches? xpr pat0 pat1 ...)
checks if the value of the expression xpr matches any of the patterns pat0 pat1 ...
er-macro-rules[syntax] (er-macro-rules (%sym ...) (code0 xpr0) (code1 xpr1) ...)
references a renamed version of sym ... under the name %sym ... and pairs the differnt macro-codes code0 code1 ... with expressions xpr0 xpr1 ..., which usually evalute to backquoted templates.
This macro is unhygienic by design, it introduces the symbol compare? into its scope.
ir-macro-rules[syntax] (ir-macro-rules (sym ...) (code0 xpr0) (code1 xpr1) ...)
pairs the differnt macro-codes code0 code1 ... with expressions xpr0 xpr1 ..., which usually evalute to backquoted templates in the scope of injected symbols sym ....
This macro is unhygienic by design, it introduces the two symbols inject and compare? into its scope.
One of[syntax] (define-syntax-with-contract name docstring rules)
where rules is one of
- (syntax-rules (sym ...) (pat0 tpl0) (pat1 tpl1) ...)
- (ir-macro-rules (sym ...) (pat0 xpr0) (pat1 xpr1) ...)
- (er-macro-rules (%sym ...) (pat0 xpr0) (pat1 xpr1) ...)
and docstring is optional,[syntax] (define-syntax-with-contract name (syntax-contract (name . rest) docstring) transformer)
where docstring is optional and transformer is a raw low-level macro-transformer,[syntax] (define-syntax-with-contract (name . rest) docstring with-expression)
where docstring is optional and with-expression is one of
- (literal syms . body)
- (with-renamed syms . body)
- (with-injected syms . body)
which will be translated to syntax-rules, er-macro-rules or ir-macro-rules respectively.
doclist[parameter] (doclist '())
should be called before the first define[-syntax]-with-contract expression to initialize automatic documentation.
doclist->dispatcher[procedure] (doclist->dispatcher (doclist))
saves (doclist) in a dispatcher. A typical use is
(define module-name (doclist->dispatcher (doclist)))
which should be called after the last define[-syntax]-with-contract expression to save the automatic documentation in module-name. This procedure can than be called by the module's client with or without a symbol argument.
Without argument the call returns the list of exported symbols, with argument the call returns the textual representaion of the contract of the module's exported symbol sym.
prints the documentation of the whole module in readable form.
contracts[procedure] (contracts [sym])
prints the contract of the exported symbol sym of the contracts module or the list of exported symbols when called as a thunk.
(use contracts) (import-for-syntax (only contacts syntax-contract er-macro-rules ir-macro-rules))
(use contacts) (import-for-syntax (only contracts syntax-contract ir-macro-rules er-macro-rules)) ;;; initialize documentation (doclist '()) ;;; a single datatype as an alternative to boxes ;; predicate (define-with-contract (single? xpr) "check, if xpr evaluates to a single" (and (procedure? xpr) (condition-case (eq? 'single (xpr (lambda (a b c) a))) ((exn) #f)))) ;; constructor (define-with-contract (single xpr) "package the value of xpr into a single object" (domain: (true? xpr)) (range: (single? result)) (lambda (sel) (sel 'single xpr (lambda (new) (set! xpr new))))) ;; query (define-with-contract (single-state sg) "returns the state of the single object sg" (domain: (single? sg)) (range: (true? result)) (sg (lambda (a b c) b))) ;; command (define-with-contract (single-state! sg arg) "replaces state of sg with arg" (domain: (single? sg) (true? arg)) (effect: (state (single-state sg) arg)) ((sg (lambda (a b c) c)) arg)) ;;; Euclid's integer division as an example for a ;;; function with two results (define-with-contract (quotient+remainder m n) "integer division" (domain: (integer? m) (not (negative? m)) (integer? n) (positive? n) (<= n m)) (range: (with-results (q r) (integer? q) (integer? r) (= (+ (* q n) r) m))) (let loop ((q 0) (r m)) (if (< r n) (values q r) (loop (add1 q) (- r n))))) ;;; some binding macros with results (bind x 1 x) ; -> 1 (bind (x (y (z . u) v) . w) '(1 (2 (3) 4) 5 6) (list x y z u v w)) ; -> '(1 2 3 () 4 (5 6)) (bind-case '(1 (2 3)) ((x (y z)) (list x y z)) ((x (y . z)) (list x y z)) ((x y) (list x y))) ; -> '(1 2 3) (bind-case '(1 (2 3)) ((x (y . z)) (list x y z)) ((x y) (list x y)) ((x (y z)) (list x y z))) ; -> '(1 2 (3)) (bind-case '(1 (2 3)) ((x y) (list x y)) ((x (y . z)) (list x y z)) ((x (y z)) (list x y z))) ; -> '(1 (2 3)) (bind-let* ( (x 1) ((y (z w)) (list 2 (list 3 x))) ) (list x y z w)) ; -> '(1 2 3 1) ;;; and some match tests with results (matches? 1 x) ; -> #t (matches? '(1 2) x) ; -> #t (matches? '(1 2) (x y z)) ; -> #f (matches? '(1 2) (x (y z))) ; -> #f (matches? '(1 (2 3)) (x y z)) ; -> #f (matches? '(1 (2 3)) (x (y . z))) ; -> #t (matches? '(1 (2 3)) (a b) (x y z) (x (y z))) ; -> #t ;;; the same trivial freeze macro implemented in different styles (define-syntax-with-contract (sefreeze xpr) "sefreeze" (with-renamed (%lambda) `(,%lambda () ,xpr))) (define-syntax-with-contract (sifreeze xpr) "sifreeze" (with-injected () `(lambda () ,xpr))) (define-syntax-with-contract (ssfreeze xpr) "ssfreeze" (literal () (lambda () xpr))) (define-syntax-with-contract sfreeze "sfreeze" (syntax-rules () ((_ xpr) (lambda () xpr)))) (define-syntax-with-contract ifreeze "ifreeze" (ir-macro-rules () ((_ xpr) `(lambda () ,xpr)))) (define-syntax-with-contract efreeze "efreeze" (er-macro-rules (%lambda) ((_ xpr) `(,%lambda () ,xpr)))) (define-syntax-with-contract lifreeze (syntax-contract (lifreeze xpr) "lifreeze") (ir-macro-transformer (lambda (f i c) `(lambda () ,(cadr f))))) (define-syntax-with-contract lefreeze (syntax-contract (lefreeze xpr) "lefreeze") (er-macro-transformer (lambda (f r c) `(,(r 'lambda) () ,(cadr f))))) (define-syntax-with-contract lfreeze (syntax-contract (lfreeze xpr) "lfreeze") (lambda (f r c) `(,(r 'lambda) () ,(cadr f)))) ;; save documantation in dispatcher (define docs (doclist->dispatcher (doclist)))
data-structures, extras, srfi-13
Jul 22, 2011
Copyright (c) 2011, Juergen Lorenz All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions 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.
THIS 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.
- changed with-literal to literal
- added bind bind-let* bind-case matches syntax-contract ir-macro-rules er-macro-rules, changed define-syntax-with-contract
- (results: ...) made obsolete, use (with-results (name ...) . body) within (range: ...) instead
- changed (effect: ...), removed (state: ...) (invariant: ...)
- some enhancements
- added print-doclist, fixed typo in setup script reported by mario
- initial import