You are looking at historical revision 23360 of this page. It may differ significantly from its current revision.
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 wrong arguments, and the routine will not even return with wrong 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 design. We'll package the needed macros and procedures in a Chicken module called contracts. The fundamental macros are called define-with-contract and define-syntax-with-contract, which replace and wrap define and define-syntax respectively. So instead of
(define name proc)
you will write
(define-with-contract name contract-expression proc)
and instead of
(define-syntax name transformer)
(define-syntax-with-contract name contract-expression transformer)
where proc is a lambda expression and transformer a syntax-rules expression in most cases. In both cases, there are short forms as well.
But before we go into the details, how such a contract-expression looks like, it should be noted, that this macro should automate the documentation of the contract to be supplied. After all, a contract without the contract document - the small print - is useless. To do this, we export a parameter, doclist, and a procedure, doclist->dispatcher, which are used by client code, preferably a module, as follows: At the start of the client module, doclist is initialized to the empty list, (doclist '()) and at the end it is saved to a dispatcher, say client, with
(define client (doclist->dispatcher (doclist))).
Between these two calls every instance of define-with-contract and define-syntax-with-contract will store its textual representation of contract-expression under the symbol name, so that a client of the client-module, client, say, can either call (client) to get a list of available names, or (client 'name) to get documentation of the name routine.
Let's start with the contract-expression above, in other words, how does a contract look like? The answer differs for procedures and macros as well as for queries and commands, or - to express this more Lisp-like - for functions (in the strict mathematical sense, i.e. without side-effects) and procedures with state, and it is different for macros as well.
Let's start with functions.
Mathematical functions have a domain and a range, Lisp functions have arguments (possibly none at all) and results (possibly more than one). The former are named in the declaration, not so the latter. So, if we want to check results, we must name them in the contract. This is done with a (results: ...) clause. If no (results: ...) clause is supplied, then it is assumed, that only one result is produced and named "result". The checks of arguments and results must involve predicates, so there are clauses (domain: ...) and (range: ...) which collect predicate-expressions on arguments and results. And last, but not least, for documentation purposes, there should be a docstring. All this should appear after the call structure of the routine to be checked, which is the only required argument.
So for Euclid's integer division, to give a typical example, the contract should look like this
(contract (quotient+remainder m n) "integer division" (results: q r) (domain: (integer? m) (not (negative? m)) (integer? n) (positive? n) (<= n m)) (range: (integer? q) (integer? r) (= (+ (* q n) r) m)))
Put together, the whole checked quotient+remainder routine will look like this
(define-with-contract quotient+remainder (contract (quotient+remainder m n) ...) ; see above (lambda (m n) (let loop ((q 0) (r m)) (if (< r n) (values q r) (loop (add1 q) (- r n))))))
You should note, that contract and implementation are strictly separated. You as the supplier can write the implementation without worrying about the parameters in the implementation, it's checked by the contract. In fact, you mustn't, it's the client's duty. On the other hand, the client can be sure, that the routine delivers the correct results, provided it runs through.
How is this black magic possible? It's simple: In Scheme, procedures are first class values. They can be arguments and results of procedures. Hence, we only need to implement the contract-expression as a macro, which returns a procedure, accepting the implementation as argument and returning the contract-checked implementation.
Isn't that a lot of checking, you might ask. Yes, it is. But you needn't include all of this checking into the ultimate compiled code. Remember, that development in Scheme is different than development in a language without an interpreter: Only after you have tested your routine interactively you'll compile it. So you'll arrange matters in such a way, that only interpreted code will check both the domain and the range, while compiled code will only test the former. Chicken allows to include interpreted-only code into an (eval-when (eval) ...) expression - a feature borrowed from Common Lisp - which provides this distinction. Moreover, if you are really concerned about speed, you can avoid domain checking as well, compiling your code with the unsafe switch, because the actual checks will be done in assert epressions, which are ignored in unsave code. But that's like driving without a security belt.
If you look at the above code, you'll note still some redundancy. So, like the short form of procedure definitions
(define (name . args) xpr . xprs)
we'll supply a short form of define-with-contract as well, omitting the contract-line and the lambda-line:
(define-with-contract (quotient+remainder m n) "integer division" (results: q r) (domain: (integer? m) (not (negative? m)) (integer? n) (positive? n) (<= n m)) (range: (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)))))
State changing procedures
Now to the commands, procedures which change state. The state may be internal, e.g. a let before the defining lambda, or external, i.e. a hidden variable in the defining module.
Now remember command-query-separation. To change the state of a routine and to return this state should be separate operations, which can conveniently separated by the number of arguments. Called with the required arguments (there might be none), the state is returned, and called with additional arguments the state is changed with those additional arguments. Hence, we'll usually define commands with a case-lambda, a chicken extension. In other words, in our model commands are in fact two routines, whence their contracts need to check two routines. That one returning the state is an ordinary query but its clauses are named a bit differently, for example
(define-with-contract inv (contract (inv) "invariant test with a computed attribute" (state: a b c) (invariant: (number? a) (number? b) (number? c) (= c (+ a b)))) (let ((a 1) (b 2)) (lambda () (let ((c (+ a b))) (values a b c)))))
The routine changing state must do this check and compare old and new values as well. Hence we have another state clause, this time listing pairs of old-new-references and an effect clause controlling the change.
Let's describe the contract and implementation of a simple command, an adder% routine which adds its argument to its state.
(define-with-contract adder% (contract (adder! arg) "adds its argument to its state" (domain: (number? arg)) (state: state) (invariant: (number? state)) (state: (old new)) (effect: (= (+ old arg) new))) (let ((state 0)) (case-lambda (() state) ((arg) (set! state (+ state arg))))))
Note, that the two (state: ...) lists must be of same length, since the pairs in the one are the values of the names of the other at different times in the computation. Note also, that a short form in this case makes no sense, since the state is internal.
Here is another example, a bit more realistic, namely an alternative to a box. This time the state is encapsulated in single-state%'s first argument and a short form makes sense.
(define-with-contract (single xpr) "package xpr in a box" (domain: #t) (range: (procedure? result) (lambda (sel) (sel 'single (case-lambda (() xpr) ((new) (set! xpr new))))))
(define-with-contract (single? xpr) "check, if xpr evaluates to a single" (and (procedure? xpr) (condition-case (eq? 'single (xpr (project 0))) ((exn) #f))))
(define-with-contract (single-state% sg . args) "replaces state of sg with (car args), returns state if (null? args)" (domain: (single? sg)) (state: state) (invariant: (true? state)) (effect: (equal? new (car args))) (if (null? args) ((sg (project 1))) ((sg (project 1)) (car args))))
What to do with macros?
As for procedures
(define-syntax-with-contract name contract-expression transformer)
should result in a checked syntax-definition including its automatic documentation.
But macros are different from procedures in many aspects. First, they operate an forms only, i.e. they accept literal lists and return lists. Second, the transformer is evaluated at preprocessing time, that is, before runtime. So it has no access to runtime values.
What are transformers? In R5RS-Scheme, they are syntax-rules expressions. Well, syntax-rules matches a series of patterns against a series of templates and returns the template of the first matching pattern. On the other hand, a domain check for a macro could only test, if the macro code, which is a list, matches some patterns. In other words, the pattern-matching of syntax-rules could be considered as a domain-check, provided we are able to expose the admissible patterns for the documentation. Exposing those patterns would considerably improve the error message in case of failure as well. After all, the standard error message
during expansion of (name ...) - no rule matches form (name ...)
is not of much help, unless we check the documentation, which, of course, must exist and be actual. The result of this considerations is, that the contract-expression doesn't need a domain clause, but the admissible patterns have to be exposed.
But what about a range clause? Does it make sense, to check the range of a macro-transformer? Well, one could match the macro-expansion against some patterns as well. But I don't think that this is worth one's efforts, since one can always check that range with a simple call of the Chicken extension expand. To sum up this discussion, the contract-expression of macros will simply be a documentation string.
All this applies to high-level syntax-rules macros only, not to raw low-level explicit renaming ones. The defining lambda expression can't export any patterns, because there are none. The solution of this problem is, that we'll have to supply them. Or, alternatively, to package the definition of low-level macros into exactly the same syntax as high-level macros. In other words, we need to supply a macro, explicit-renaming, with exactly the same syntax as syntax-rules and use it like this
(define-syntax name (explicit-renaming (%sym ...) (pat xpr) (pat1 xpr1) ...)
where each sym is a symbol to be renamed and %sym represents its renamed version (any other one-character prefix will work as well). Each xpr, xpr1, ... on the other hand, is a procedure of one argument, compare?. Like syntax-rules, this macro should expand into a lambda-expression with the standard three arguments form, rename, compare?.
To give a nontrivial example, the ordinary definition of a do-for macro with explicit renaming could look like this
(define-syntax do-for (explicit-renaming (%let %loop %unless %+ %>= %stop) ((_ var (start stop . steps) . body) (lambda (compare?) (let ((step (if (null? steps) 1 (car steps)))) `(,%let ((,%stop ,stop)) (,%let ,%loop ((,var ,start)) (,%unless (,%>= ,var ,%stop) ,@body (,%loop (,%+ ,step ,var))))))))))
and a hygienic low-level or macro like this
(define-syntax our-or (explicit-renaming (%if %my-or) ((_) (lambda (compare?) #f)) ((_ arg . args) (lambda (compare?) `(,%if ,arg ,arg (,%my-or ,@args))))))
By the way, using this macro, explicit-renaming, we'll avoid the tedious work of destructuring the macro-code by hand and facilitate the renaming as well.
The implementation of explicit-renaming is not hard, provided there is some help with pattern matching. The Chicken egg matchable exports a macro, match, which might do that job.
Now, we have unified the definition of high- and low-level macros and can process them in the same way.
The short form of define-syntax-with-contract is easy insofar, as the contract-expression is simply a mandatory docstring. But this short form is possible only for transformers with one pattern only. There still remains the problem, what to do with the identifier arguments. Well, in syntax-rules, most of the time there are none, so we consider only this case for syntax-rules (like in Chicken's define-syntax-rule). In sum, the syntax is one of
(define-syntax-with-contract (name . rest) docstring xpr)
(define-syntax-with-contract (name . rest) xpr) (define-syntax-with-contract name transformer)
where transformer is a syntax-rules or an explicit-renaming expression.
contract[syntax] (contract (name . args) . xprs)
where args is a lambda-list and xprs can contain any of the following expressions
- a docstring
- a list of domain checks (domain: assumption ...)
- a list of result names (results: result0 result1 ...), if not supplied (results: result) is assumed
- a list of range checks (range: proposition ...)
- a list of state attributes (state: attribute0 attribute1 ...)
- a list of invariant checks (invariant: inv ...)
- a list of state old-new-pairs (state: (old0 new0) (old1 new1) ...) of the same length as the state-attributes list
- a list of side-effect checks (effect: change ...)
define-with-contract[syntax] (define-with-contract name contract proc)
[syntax] (define-with-contract (name . args) contract-clause ... . body)
checks the procedure proc with contract, appends contract to the documentation (via doclist), and defines name as the checked procedure. The short hand version makes sense only for queries.
define-syntax-with-contract[syntax] (define-syntax-with-contract name docstring transformer)
[syntax] (define-syntax-with-contract (name . rest) docstring xpr)
where transformer is either a syntax-rules or an explicit-renaming espression. Registers transformer as a syntax-transformer under name, after having collected docstring and the transformer's pattern forms in (doclist). The second case evaluates to syntax-rules.
parameter, which produces an empty list to be populated by define-with-contract with the '(name [docstring] [contract]) lists.
doclist->dispatcher[procedure] (doclist->dispatcher alist)
transforms an association list, e.g. constructed by (doclist), into a dispatcher routine, which prints the association's values.
Prints actual parameter doclist in readable form.
contracts[procedure] (contracts [sym])
documentation procedure. Returns the list of available symbols if called with no arguments and i.a. the call structure of a macro, if called with the macro's name
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.
- added print-doclist, fixed typo in setup script reported by mario
- initial import