contracts

This extension provides basic support for contract-oriented programming. Definitions can be grouped into a contract which specifies what preconditions should be met when an exported procedure is called from outside the group, as well as what post-conditions and invariants have to be fulfilled when a call to an exported procedure returns.

contracted

[syntax] (contracted CLAUSE ...)

Defines a group of definitions that share a contract. Each CLAUSE should be one of the following:

define/contract

[syntax] (define/contract (NAME ARGUMENT ...) [-> RESULT] BODY ...)

Defines a single function with a contract. ARGUMENT may be eithe a symbol (equivalent to (any? SYMBOL)) or a list of the form (PROCEDURE SYMBOL) which specifies the variable name and precondition predicate. The optional RESULT designates a predicate on the result as a post-condition.

export

[contract clause] (export ((NAME ARGUMENT ...) [-> RESULT ...]) ...)

Exports the procedure NAME from the contract group. ARGUMENT should evaluate to a procedure that is called on the argument at the given position and which must succeed (i.e. return a value distinct from #f) for the precondition to hold. If the argument predicate returns #f an exception is signalled by invoking contract-violation (see below). RESULT should evaluate to a procedure that must return true for the result at the designated position when the invocation of NAME returns. If no -> RESULT ... is given, the procedure is expected to return a single unspecified result.

export*

[contract clause] (export* ((NAME ARGUMENT ...) [-> RESULT ...]) ...)

Identical to export but also exports the procedure NAME when used during compilation by generating a (declare (export NAME)) form in the expansion of the contract body.

invariant

[contract clause] (invariant EXPRESSION)

Defines an invariant: EXPRESSION must return true after any call to an exported procedure or a contract violation is signalled.

definition

[contract clause] (define ...)

Defines an exported or non-exported entity. Note that all definitions have non-toplevel semantics. If no definition of an exported procedure is found a warning will be signalled (since macros may expand into definitions, the resulting code may still be valid).

form

[contract clause] EXPRESSION

An arbitrary expression in the contract body. Depending on the macro-expander used this may (default low-level macros) or may not (syntax-case, syntactic-closures) be followed by more definitions.

contract-violation

[procedure] (contract-violation CONTRACT LOCATION MESSAGE FORM [ARGUMENT ...])

Signals a contract violation condition of the kinds (exn contract-violation). The contract-violation condition has the property NAME which contains the CONTRACT argument as value. CONTRACT should be a string or symbol that names the contract, LOCATION a symbol designating the procedure where the contract violation occurred (or #f). MESSAGE should be a string and FORM the expression that produced the contract violation (or some hint at the failed expression). Any extra ARGUMENTs are stored as the arguments condition property in the condition.

Notes

Argument lists in export clauses may contain DSSSL lambda-list markers (#!optional, #!rest and #!key) - in fact rest-argument predicates can only be specified using #!rest since dotted list syntax would be ambiguous. Keyword arguments should be specified as (SYMBOL PREDICATE).

Calls to exported definitions go through an intermediate wrapper procedure and are never in tail-position.

By defining the feature disable-contracts (in the interpreter either by evaluating (register-feature! 'disable-contracts) or via the -D csi option, or in the compiler by using the -D or -feature options), pre- and postconditions and invariants are not checked.

Example

;;;; stack.scm

(use srfi-1 contracts)

(contracted
 (export ((stack-push #!rest (list-of number?)))
	 ((stack-pop) -> number?)
	 ((stack-size) -> integer?)
	 ((stack-empty) -> boolean?) )
 (define *the-stack* '())
 (define check-stack
   (let ((numlist? (list-of number?)))
     (lambda () (numlist? *the-stack*)) ) )
 (invariant (check-stack))
 (define (stack-push . ns)
   (set! *the-stack* (append-reverse ns *the-stack*)) )
 (define (stack-pop)
   (assert (not (null? *the-stack*)))
   (let-values (((x more) (car+cdr *the-stack*)))
     (set! *the-stack* more)
     x) )
 (define (stack-size) (length *the-stack*))
 (define (stack-empty) (null? *the-stack*)) )

Author

felix winkelmann

License

BSD

History

0.2
Added define/contract
0.1
Initial version