You are looking at historical revision 28109 of this page. It may differ significantly from its current revision.
- Design by Contract
- The syntax
- How do all these macros work?
- How to organize your code?
- Another example
- Exported routines
- Initial version
- Version History
Design by Contract
Design by Contract is a programming paradigm invented by Bertrand Meyer for his purely Object Oriented Language Eiffel. The objective is to reduce the complexity of software by means of a clear separation of concerns between its suppliers and clients. One of the rules is: Never do a check an both sides of the abstraction barrier. To achieve this, Eiffel fosters a style, in which each routine clearly specifies, what are the assumptions (preconditions) of a routine and what are its propositions (postconditions). Moreover, the runtime system is able to check these conditions. If now a routine call fails because of illegal arguments, the client is to blame, but if it fails with violated propositions, it is the supplier's fault. The routine's body will not even be accessed with violated assumptions , and the routine will not even return with violated propositions.
The metaphor is that of a contract between supplier and client. The supplier guarantees correct results, provided the client fulfills his duties. If not, the supplier is not obligated to start work at all. As in real life, both parties need a copy of the contract, and there must be a judge in case of troubles. Translated to programming, this means, the contract needs to be documented, and both parties can trust each other, so that they need not - and should not - check the other's duties, the runtime system will do it. It's a bit like proving a mathematical theorem: to prove its proposition, the assumptions can be taken for granted. Without them, the proposition is simply meaningless.
There is still another metaphor of Meyer's, Command-Query-Separation. That means, that the programmer should never write routines both for a result and for a side-effect (like the ++ operators in C). Instead, two routines should be written, one that returns a result, the other that changes state. The former are called queries by Meyer, the latter commands (because all of Eiffel's routines operate on objects, they either query or command its state). In Scheme we have functions without side-effect, written for their results only (the recommended style), and state-changing procedures, which are normally denoted with a trailing bang. But independent of the different terminology, the principle applies to Scheme as well, in fact to every language.
Design by Contract is such a powerful paradigm, that anybody, who ever has programmed in Eiffel, would like to have it in his favorite language. Outside the Lisp family of languages, you where out of luck, but Lisps, being programmable programming languages, allow you to add to the language what you miss. In Lisp, you are a language designer as well as a programmer! In what follows, you'll see, how easy it is to implement Design by Contract in Chicken Scheme.
Let's start with the interface. We'll package the needed macros and procedures into a Chicken module called dbc. The fundamental macros are called contract (for functions), command-contract (for commands) and macro-contract (for low-level macros). Their syntax is similar to the syntax of syntax-rules as explained below.
There are no contracts for high-level macros, because the pattern matching process of syntax-rules can be considered as precondition checking. After all, macros are evaluated at compile time, i.e. before runtime. Hence they have no access to an expression's value, they treat expressions as literal lists. Hence preconditions can only check, if those expressions match some patterns .... But something should be done to document the accepted patterns, since syntax-rules' error messages
during expansion of (name ...) - no rule matches form: (name ...)
don't help without documentation: push-contract! can provide the necessary documentation by hand.
These contract macros are used with
(define-with-contract contract-expression procedure)
for both procedure types and
(define-macro-with-contract macro-contract-expression macro-transformer-expression).
All these macro calls must be enclosed into two other macro calls, (init-dbc) and (exit-dbc-with name). The first macro is unhygienic, because its call will define a global variable, *contracts*, to collect the documentation of contracts, and it will initialize a special exception-handler. The second macro call will store the collected documentation in a dispatcher, name, by convention the module name. The call (name) will then list the documented symbols, (name 'sym) the documentation of sym and (name "file") will store the whole documentation in file in a wiki like format.
Note that automatic documentation is essential for design by contract. After all, a contract without a contract document, the "small print" is useless.
Above I said, that the syntax of contract expressions is similar to the syntax of syntax-rules
(syntax-rules (key ...) (pat0 tpl0) (pat1 tpl1) ...)
where pat0, pat1 ... are nested lambda-lists and tpl0, tpl1, ... the templates to be generated by the macro for the first pattern matching the macro's use.
A macro-contract expression changes the templates to matchers, i.e. routines which check, if the macro expansion matches some nested lambda-list and eventually some additional conditions. The matches? macro will do that job. Moreover, the patterns pat0, pat1 ... must eventually pass some fenders to be considered a match (this is an extension well known from syntax-case macros of R6RS). And last, but not least, low-level macros might be unhygienic, and the "dirty" symbols which pollute the name-space should be documented. In sum, macro-contracts look like this, if we use pseudo-variables .. and .... (besides ellipses, ..., "repeat the pattern on the left zero or many times") to mean "repeat the pattern to the left zero or one times, or one or many times" respectively.
(macro-contract hyg ... (key ...) (pat fender matcher) ....)
Functions without side effect are controlled by
(contract (result ....) (pat pre post) ....)
where pat is now a lambda-list, pre a precondition and post a postcondition, pre an expression checking the pattern variables of pat, and post checking the results. Note that pre might refer to the pattern variables of pat and post additionally to result .... Since strings and symbols always return #t, you can use them as pre- or postconditions.
Commands, i.e. procedures without return values, which change some state variables instead, require the most complex contract. We need to check, which state variables are changed and how. Now, commands are usually accompanied by queries, which are functions operating on a subset of the command's arguments and returning state. For example, to set-car! corresponds car, which might be used to control what set-car! changes. In sum, command-contract looks as follows
(command-contract ((old new query) ....) (pat pre post) ....)
where now post operates on the pattern variables of pat as well as the old and new variables. But here remains one twist: The macro can't know, on which subset of the command's arguments the queries operate. We must tell it. In other words, the supplied queries must be lifted to command's argument list.
Note that despite their similarities, there is one difference in the postconditions of these three contract macros: procedure contracts require an expression, while macro-contract requires a predicate, i.e. a function.
Let's consider an example, a function with two return values, Euclid's integer division. Note that this contract proves, that the function does what it is supposed to do!
(define-with-contract q+r (contract (q r) ; two results ((_ m n) (and ; preconditions (integer? m) (not (negative? m)) (integer? n) (positive? n) (<= n m)) (and ; postconditions (integer? q) (integer? r) (= (+ (* q n) r) m)))) (lambda (m n) (let loop ((q 0) (r m)) (if (< r n) (values q r) (loop (+ q 1) (- r n))))))
How do all these macros work?
Well, it's relatively simple. The three contract expressions return a pair, consisting of its own documentation and a procedure. The latter does the actual checks. In other words, it accepts another procedure as argument and returns that very procedure with annotated checks.
The two defines store the contract's documentation in *contracts*, supplied by init-dbc, and apply the contract's checker to its procedure argument.
Isn't that a lot of checking code, you might ask, and you are right. Therefor there is a parameter, contract-check-level, with values 0, 1 and 2, meaning "no checks at all, only documentation", "check only preconditions" or "check everything" respectively. The default is 1, but in the developing phase you'll probably set it to 2.
How to organize your code?
Typically, you'll place the raw definitions without any defenses in one module, say raw-foo, and import their names with a prefix into another one, say foo, to add the contracts to them. These prefixed names can than be used in foo's contracts as well. The second module, foo, is the one to be exported.
The splitting into two modules has several advantages. First, it helps developing. Usually, you'll have an idea, what a routine should do and how to implement it. At this stage, you needn't bother about "defensing programming" or anything like this, you can add the defenses later. You can already test your ideas incrementally and see if they do what they are supposed to do.
Second, you wouldn't like to check these defenses again and again in your own routines, in particular in recursive ones. It's better to do the checks only once from outside.
Third, you can enhance your old modules with contracts later one without touching the code.
Fourth, if you like driving without a security belt and are concerned with speed, you can import raw-foo instead of foo into client code.
The following rather contrieved example may clarify this. The resulting module, foo, contains all three contract types.
(module raw-foo (adder adder! freeze) (import scheme) (define state 0) (define (adder) state) (define (adder! n) (set! state (+ state n))) (define (freeze form inject compare?) `(lambda () ,(cadr form))) ) ; end raw-foo
Then you define and add the contracts to the prefixed names
(module foo (adder adder! freeze) (import (prefix (except raw-foo freeze) "%")) (import-for-syntax (prefix (only raw-foo freeze) "%")) (define-with-contract adder (contract (result) ((_) #t (number? result))) %adder) (define-with-contract adder! (command-contract ((old new (lambda (n) (%adder)))) ((_ n) (number? n) (= new (+ old n)))) %adder!) (define-macro-with-contract freeze (macro-contract () ((_ x) #t (matches? (lambda () x)))) (ir-macro-transformer %freeze)) ) ; end foo
command-contract[syntax] (command-contract ((old new query) ....) (pat pre post) ....)
hygienic, keys ()
(command-contract ((old new query) ....) (pat pre post) ....) (lambda-list? pat) (contract? result)
contract[syntax] (contract (result ....) (pat pre post) ....)
hygienic, keys ()
(contract (result ....) (pat pre post) ....) (lambda-list? pat) (contract? result)
contract-arguments[procedure] (contract-arguments cnd)
(contract-arguments cnd) (contract-condition? cnd) (list? result)
contract-check-level[parameter] (or (contract-check-level) (contract-check-level x))
(or (result) ((old new (lambda (x) (contract-check-level)))))
(contract-check-level) (and (integer? result) (<= 0 result 2) "0: no checks, 1: preconditions checked, 2: pre- and postconditions checked") (contract-check-level x) (and (integer? x) (<= 0 x 2)) (= new x)
contract-condition-handler[procedure] (contract-condition-handler exn)
(contract-condition-handler exn) (condition? exn) "result of handled exeption"
contract-condition?[procedure] (contract-condition? xpr)
(contract-condition? xpr) #t (boolean? result)
contract-location[procedure] (contract-location cnd)
(contract-location cnd) (contract-condition? cnd) (symbol? result)
contract-text[procedure] (contract-text cnd)
(contract-text cnd) (contract-condition? cnd) (string? result)
contract?[procedure] (contract? xpr)
(contract? xpr) #t (boolean? result)
define-macro-with-contract[syntax] (define-macro-with-contract name contr (transformer-type proc))
hygienic, keys ()
(define-macro-with-contract name contr (transformer-type proc)) (contract? contr) (begin (push-contract! (car (contr (quote name)))) (define-syntax name (transformer-type ((cdr (contr (quote name))) proc))))
define-with-contract[syntax] (define-with-contract name contr proc)
hygienic, keys ()
(define-with-contract name contr proc) (contract? contr) (begin (push-contract! (car (contr (quote name)))) (define name ((cdr (contr (quote name))) proc)))
exit-dbc-with[syntax] (exit-dbc-with name)
hygienic, keys ()
(exit-dbc-with name) (symbol? name) "saves *contracts* in dispatcher name"
not hygienic, exports *contracts*, keys ()
(init-dbc) #t "initializes exception handler"
lambda-list?[procedure] (lambda-list? xpr)
(lambda-list? xpr) #t (boolean? result)
macro-contract[syntax] (macro-contract hyg ... (key ...) (pat fender matcher) ....)
hygienic, keys ()
(macro-contract hyg ... (key ...) (pat fender matcher) ....) (and (nested-lambda-list? pat) (procedure? matcher)) (contract? result)
make-contract-condition[procedure] (make-contract-condition location text . arguments)
(make-contract-condition location text . arguments) (and (symbol? location) (string? text)) (condition? result)
make-dispatcher[procedure] (make-dispatcher alist)
(make-dispatcher alist) ((list-of? list?) alist) (procedure? result)
matches?[syntax] (matches? pat . fenders)
hygienic, keys ()
(matches? pat . fenders) (nested-lambda-list? pat) "procedure returning #t if its argument matches pat with fenders"
nested-lambda-list?[procedure] (nested-lambda-list? xpr)
(nested-lambda-list? xpr) #t (boolean? result)
push-contract![syntax] (push-contract! contract-docu)
hygienic, keys ()
(push-contract! contract-docu) "documentation of a contract" (matches? (set! *contracts* (cons contract-docu *contracts*)))
string-repeat[procedure] (string-repeat str n)
(string-repeat str n) (and (string? str) (not (negative? n))) (string? result)
Jan 10, 2013
Copyright (c) 2013, 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.
- initial import