1. Design by Contract
  2. Command-query-separation
  3. The dbc module
    1. The syntax
      1. Macro contracts
      2. Function contracts
      3. Command contracts
      4. A first example
      5. How do all these macros work?
      6. How to organize your code?
      7. Another example with two modules
  4. Author
  5. Initial version

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.

Command-query-separation

There is another metaphor of Meyer's, Command-Query-Separation: 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 anyone who has ever programmed in Eiffel, would like to have it in his favorite language. Outside the Lisp family of languages, you are out of luck, but Lisps, being programmable programming languages, allow you to add features to the language. 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 dbc module

This egg is an attempt, to bring DbC to CHICKEN Scheme. A module written in this style - let's call it "example" in this turorial - has to import dbc. Its body should be enclosed in

(init-dbc)
...
(exit-dbc-with example)

which guarantees, that documentation is automatically collected and saved in a dipatcher routine, by convention the module's name. Calling the dispatcher with no arguments returns a list of the exported symbols, with one of these symbols, it returns the symbol's documentation and called with a string it saves the skeleton of wiki-documentation in a file with the string's name.

This automatic documentation is essential for DbC, after all a contract without a treaty, i.e. the "small print" is useless, since both parties need to know and accept their rights and duties.

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

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.

Macro contracts

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

Function contracts

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.

Command contracts

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.

A first 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 a module-global variable *contracts*, supplied by init-dbc (which must therefore be unhygienic), 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,

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

Another example with two modules

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


(require-library dbc)

(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

Author

Juergen Lorenz

Initial version

Jan 15, 2013