[plt-scheme] Design by Contract for Functions in DrScheme

[Robert Bruce Findler <robby@cs.rice.edu>]

As you may have noticed from a recent post about a contract violation,
DrScheme now supports a Design by Contract-like mechanism for
higher-order functions. We have been experimenting with it internally
for several months now, and just over the last week I've added more
than a hundred contracts to the framework (one of the larger libraries
inside DrScheme).

Contracts in DrScheme are dynamically checked. They are either
predicates that determine the fitness of (flat) values, or higher-order
contracts that constrain the behavior of functions. Predicate contracts
are just single-argument lambda's that return booleans. Higher-order
contracts are constructed with the -> constructor. For example, this
contract:

     ((greater-than-10? . -> . greater-than-100?)
      . -> .
      greater-than-100?)

matches functions that accept functions as arguments. The input
function must map numbers greater than 10 to numbers greater than 100
and the entire function must also produce numbers greater than zero.

Here's how you'd use that contract:

(module m mzscheme
  (require (lib "specs.ss" "framework"))
  (define (greater-than-100? x) (and (number? x) (x . > . 100)))
  (define (greater-than-10? x) (and (number? x) (x . > . 10)))

  (provide/contract 
   (f ((greater-than-10? . -> . greater-than-100?)
       . -> .
       greater-than-100?)))
  
  (define (f g) (g 35)))

That module provides `f' with the above contract. Here are two client
modules. This one:

(module n mzscheme
  (require m)
  (f (lambda (x) (+ x 90))))

meets the contracts and no error is signaled. This one, however:

(module o mzscheme
  (require m)
  (f (lambda (x) 0)))

passes a bad argument to `f' -- the argument function doesn't always
produce numbers greater than 100. Requiring `o' produces this error:

  contract-error: blame: o; 
  contract established at: #<syntax:19:4> f; 
  predicate #<procedure:greater-than-100?> failed for: 0

The contract system correctly identifiers `o' as the faulty module and
provides a witness to the failed contract (zero).

Help Desk gives the detail for using contracts in DrScheme (including
other variants of the -> contract constructor and combinators for
building flat contracts). A submission to this year's ICFP (available
on request) gives a more id-depth overview than the above, plus more
technical details.

Robby