You are looking at historical revision 24213 of this page. It may differ significantly from its current revision.

Design by Contract

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, this software contract must be documented, 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 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)!

We will not check the macro's range, because that would need another matching process.

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 expressiong

(domain: assumption ...)
[(results: name ...)]
(range: 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 ... (if this clause is not supplied (results: 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.

(import contracts)

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

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

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

Author

Juergen Lorenz

Initial version

Jun 23, 2011

Updated

Jun 24, 2011