chicken-users
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Chicken-users] Rough proposal for contracts in Chicken


From: John Cowan
Subject: [Chicken-users] Rough proposal for contracts in Chicken
Date: Tue, 19 Dec 2006 13:22:31 -0500
User-agent: Mutt/1.3.28i

I've read over the PLT Scheme approach, and I think I see how it can be
adapted to Chicken.  Basically, the syntax of the export declaration is
extended to provide per-procedure argument and result checking, and a
new declaration is added to provide module invariants.

Currently, the export declaration takes a sequence of symbols to be
exported.  The extension is to allow lists as well as symbols, with the
following syntax:

        <export>  = (export {SYMBOL | (SYMBOL <contract>)} ...)
        <contract> = (-> (<pred> ...) <pred>) |
                (-> (<arg> ...) (<pred> ...)) |
                (and <contract> ...) | (or <contract> ...)
        <pred> = a Scheme expression evaluating to a predicate

The first form of contract says that the symbol is bound to a procedure
whose arguments satisfy the predicates in the list and whose result
satisfies the single predicate.  The second form is equivalent, but
supports a list of result predicates for use with multiple values.
In either case, the argument-predicate list may be an improper list,
with the same rules as a Scheme lambda-list.

The third and fourth form allow boolean combination of contracts.

Here are a few simple examples:

        (export (plus (-> (number? number?) number?))
                (plus/all (-> (number? . (list-of number?)) number?))
                (exact->div0+mod0 (-> (exact? exact?) (exact? exact?))))

The invariant declaration takes the form

        <invariant> = (invariant <pred> ...)

and specifies a predicate which must be true after invoking any
exported function  that has a contract.  For example:

        (declare (invariant (= 0 (length local-stack))))

compels the module variable local-stack to be a list of length 0
whenever the module exits.

The implementation provides a wrapper around each function to be
exported which is invoked whenever the function is called from outside
the module.  It consists of calls to "ensure" for each of the arguments,
followed by a call to the unwrapped function, followed by calls to
"ensure" for the return value(s), followed by calls to "assert"
for each of the invariants.

This is simple, but captures preconditions and post-conditions
as well as invariants, the core of programming by contract.
New forms of contracts, such as argument interdependency or dependency
of results on arguments, can be added later.

It would also be helpful to provide a few helper predicates and predicate
combinators, such as:

        (define (any? x) #t)

We already have list-of available (in unit extras) for use with
rest arguments.

What do you think?

-- 
Some people open all the Windows;       John Cowan
wise wives welcome the spring           address@hidden
by moving the Unix.                     http://www.ccil.org/~cowan
  --ad for Unix Book Units (U.K.)
        (see http://cm.bell-labs.com/cm/cs/who/dmr/unix3image.gif)




reply via email to

[Prev in Thread] Current Thread [Next in Thread]