Design by Contract

Design by Contract
Command-query-separation
The contracts module
The case of procedures
The case of macros
Author
Initial version
Updated

Design by Contract - DbC for short - is a metaphor introduced by Bertrand Meyer for its purely object-oriented language Eiffel. The idea consists in strictly separating the concerns of clients and suppliers of code. The supplier of a routine is not obliged to check the validity of its arguments, that's the clients duty. And in fact the supplier mustn't do it to avoid double checks. On the other hand, the supplier has to guarantee correct results of his or her routine, the client can rely on it. It's like a contract between two parties. But like a contract in social life, the "small-print" is part of the contract, hence this software contract must be documented automatically, so that each party knows each-others duties and benefits.

Command-query-separation

Another idea of Meyer's is command-query-separation, where he names a function without side-effect a "query" (it returns part of the state of his objects) and a procedure without returned value acting by side-effect only a "command" (it changes the state of his objects). His suggestion is never to do both in one routine (like the ++ operators in C), write two instead. This is a suggestion only, it can not be enforced.

The contracts 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 contracts. Its body should be enclosed in

(doclist '())
...
(define example (doclist->dispatcher (doclist)))

where doclist is a paramter, to generate automatic documentation. This documentation can be accessed by the client in two ways. First by calling (example) without arguments, returning the list of all symbols, exported by the example module, second by calling (example 'foo) returning a representation of foo's contract provided foo is an exported symbol.

Well, this contracts must be supplied, before their representations can be exported. This is done by replacing define and define-syntax in the module body with define-with-contract and define-syntax-with-contract. And of course, these latter macros must contain the actual contracts in some way.

The case of procedures

The contracts module supplies a short and a long form of define-with-syntax, where the short form looks like this

(define-with-contract (foo . args) clause ... . body)

where each clause is either a docstring or one of the following expressions

(domain: assumption ...)
(range: proposition ...) or (range: (with-results (name ...) proposition ...))
(effect: (state query change [equ?]) ...)

The assumption ... expressions check the assumptions (including the types) of the arguments args, the proposition ... expressions the result-names name ... (without with-results the one result name "result" is assumed) and the (state query change) triples the change of the variable state initialized with the query expression before the command call to its value after the command call. Comparison is done with equal? [or equ?, if that argument is supplied]. Note, that the effect: triples are similar to the triples in the declaration part of do.

Note that command-query-separation demands, that at most one of a range: and an effect: clause is supplied.

The long form of define-with-contract looks like this

(define-with-contract foo
  (contract (foo . args)
    clause
    ...)
  (lambda args . body))

where the clauses are the same as in the short form.

Here is a nontrivial example, the implementation of the single datatype, which allows to encapsulate a value and change it as well.

(use contracts)

;;; initialize documentation
(doclist '())

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

;;; save documentation in a dispatcher
(define singles (doclist->dispatcher (doclist)))

Here is another example, a function with two results, Euclid's integer division.


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

Up to now, we have used keywords domain:, range: and effect: to implement the contracts. If you don't like them, you can use symbols domain, range and effect as well.

The case of macros

It's easy for syntax-rules macros. After all, matching the macro-code against some patterns is already a domain check! Since macro transformers have only access to forms, not to runtime values, only the forms can be checked. Consequently we have to do only two things, supply a docstring for documentation and export the admissible macro-codes, which can be extracted from the patterns. In sum, checked macros are defined in example's body like this

(define-syntax-with-contract foo
  "docstring"
  (syntax-rules () (code xpr) ...))

the only difference to define-syntax being the mandatory docstring - but the textual representations of code ... will be exported by a call to (example 'foo)!

Contracts of low-level macros are harder to implement. After all we have to destructure the macro-code by hand and take care of all the renaming. Since the macro-transformer doesn't expose admissible patterns, we either must supply and check them or we must package the destructuring and renaming into a macro with the same syntax as syntax-rules. Then we can handle it like syntax-rules. But to do this, we need other macros like destructuring-bind in Common Lisp or match in the matchable package.

The contracts module will export all the necessary means to do the job, namely binding constructs, bind and bind-case (in fact, only restricted versions of them, more powerfull ones are located in the bindings module) as well as the macros ir-macro-rules and er-macro-rules which mimic syntax-rules. To use the latter two we must import them for syntax.

Like in the case of functions there should be short forms of define-syntax-with-contract as well.

The following examples show how a trivial freeze macro could be implemented in all these variants. If you run it, you should inspect the documentation as well by calling syntax-contracts-test with or without a symbol. And you should supply wrong macro-calls like (efreeze 1 2) to see the error messages ....


(use contracts)
(import-for-syntax
  (only contracts er-macro-rules ir-macro-rules))

(doclist '())

(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-contracts-test (doclist->dispatcher (doclist)))

You might have noticed, that we didn't check a macro-transformer's range. That can be done but it would need another matching process. And that would be overkill. After all, we can inspect that range with an expand call.

Up to now I've only noted, that the contract representations are exported for documentation. But of course, the routine's contracts check the routine's implementation behind the scene, delivering meaningful error-messages in case of troubles.

You might argue, that this is a lot of error checking. And you are right. But chicken has an interpreter besides a compiler. So the contracts module arranges the checks in such a way, that only the interpreter checks propositions and assumptions, whereas in compiled code only the latter are checked.

If you are still concerned about speed of compiled code, you can compile with the unsafe switch, disabling domain checks as well. But this is like driving without a security belt ...