chickadee » dbc

Outdated egg!

This is an egg for CHICKEN 4, the unsupported old release. You're almost certainly looking for the CHICKEN 5 version of this egg, if it exists.

If it does not exist, there may be equivalent functionality provided by another egg; have a look at the egg index. Otherwise, please consider porting this egg to the current version of CHICKEN.

dbc

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.

The syntax

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

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:

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.

Example

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 %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.

Off course, you can work the other way as well: Write the interface module with the contracts first, using prefixed names for the routines to be implemented in and imported from the raw implementation module. This is the official code development strategy.

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 without touching the code.

Fourth, if you like driving without a security belt and are concerned with speed, you can import %foo instead of foo into client code.

Another example

The following rather contrieved example may clarify this. The resulting module, foo, contains all three contract types.

  (module %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 %foo

Then you define and add the contracts to the prefixed names

  (module foo (adder adder! freeze)
  (import (prefix (except %foo freeze) "%"))
  (import-for-syntax (prefix (only %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

Exported routines

command-contract

(command-contract ((old new query) ....) (pat pre post) ....)syntax
hygienic, keys ()
requires (lambda-list? pat)
ensures  (contract? result)

contract

(contract (result ....) (pat pre post) ....)syntax
hygienic, keys ()
requires (lambda-list? pat)
ensures  (contract? result)

contract-arguments

contract-arguments cndprocedure
function (result)
requires (contract-condition? cnd)
ensures  (list? result)

contract-check-level

contract-check-level x ..parameter
requires (and (integer? x)
              (<= 0 x 2)
              "0: no checks"
              "1: preconditions checked"
              "2: pre- and postconditions checked")

contract-condition-handler

contract-condition-handler exnprocedure
function (result)
requires (condition? exn)
ensures  result of handled exeption

contract-condition?

contract-condition? xprprocedure
function (result)
requires #t
ensures  (boolean? result)

contract-location

contract-location cndprocedure
function (result)
requires (contract-condition? cnd)
ensures  (symbol? result)

contract-text

contract-text cndprocedure
function (result)
requires (contract-condition? cnd)
ensures  (string? result)

contract?

contract? xprprocedure
function (result)
requires #t
ensures  (boolean? result)

define-macro-with-contract

(define-macro-with-contract name contr (transformer-type proc))syntax
hygienic, keys ()
requires (contract? contr)
ensures  (begin (push-contract! (car (contr (quote name)))) (define-syntax name (transformer-type ((cdr (contr (quote name))) proc))))

define-with-contract

(define-with-contract name contr proc)syntax
hygienic, keys ()
requires (contract? contr)
ensures  (begin (push-contract! (car (contr (quote name)))) (define name ((cdr (contr (quote name))) proc)))

exit-dbc-with

(exit-dbc-with name)syntax
hygienic, keys ()
requires (symbol? name)
ensures  saves *contracts* in dispatcher name

init-dbc

(init-dbc)syntax
unhygienic, exports *contracts* keys ()
requires #t
ensures  initializes exception handler

lambda-list?

lambda-list? xprprocedure
function (result)
requires #t
ensures  (boolean? result)

macro-contract

(macro-contract hyg ... (key ...) (pat fender matcher) ....)syntax
hygienic, keys ()
requires (and (nested-lambda-list? pat) (procedure? matcher))
ensures  (contract? result)

make-contract-condition

make-contract-condition location text #!rest argumentsprocedure
function (result)
requires (and (symbol? location) (string? text))
ensures  (condition? result)

make-dispatcher

make-dispatcher alistprocedure
function (result)
requires ((list-of? list?) alist)
ensures  (procedure? result)

matches?

(matches? pat . fenders)syntax
hygienic, keys ()
requires (nested-lambda-list? pat)
ensures  procedure returning #t if its argument matches pat with fenders

nested-lambda-list?

nested-lambda-list? xprprocedure
function (result)
requires #t
ensures  (boolean? result)

push-contract!

(push-contract! contract-docu)syntax
hygienic, keys ()
requires documentation of a contract
ensures  (matches? (set! *contracts* (cons contract-docu *contracts*)))

string-repeat

string-repeat str nprocedure
function (result)
requires (and (string? str) (not (negative? n)))
ensures  (string? result)

Author

Juergen Lorenz

Last update

Jul 08, 2014

License

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.

Version History

1.0.3
document-contracts changed
1.0.2
document-contracts changed again, run-tests used
1.0.1
document-contracts changed
1.0
initial import

Contents »