Design-by-Contracts for R7RS Scheme.
This adds functionality to add pre- and post-condition contracts to functions, in a manner similar to Ada's subprogram contracts.
View additional details at the project's repository.
TODO: Add type contracts for records and/or atoms.
Define a lambda expression as with lambda, however add
precondition and/or postcondition contracts.
Given a (pre contracts ...), where contracts ... is zero
or more expressions, evaluate each thunk sequentially in the same scope
as the function body. If an expression returns #f, then raise
an exception noting a precondition violation with the irritants being the
(quoted) expression that failed.
Given a (post contracts ...), where contracts ... is zero
or more predicate functions taking a single argument, evaluate each
contract sequentially given the return value of the function; in the
same scope as the function body and after the function has completed
evaluation. If a predicate returns #f, then raise an exception
noting a postcondition violation with the irritants being the expression
that failed and the original return value.
The contracts are short-circuit evaluated, i.e. they are evaluated sequentially from left to right and evaluation terminates if a contract fails. As such, it is recommended to have contracts sorted from most general to most specific.
A continuation captured within the function will include the postcondition checks.
Example:
(define add-map
(lambda-contract lists
(pre (every list? lists)
(>= (length lists) 2)
(apply = (map length lists)))
(post list?
(lambda (ret) (= (length ret) (length (car lists)))))
(apply map + lists)))
(add-map '(1 2 3) '(4 5 6)) => (5 7 9).
(add-map '(1 2 3) '(4 5)) => Error: precondition assertion violation: (apply = (map length lists)).
(add-map '(1 2 3) 1) => Error: precondition assertion violation: (every list? lists)
(add-map '(1 2 3)) => Error: precondition assertion violation: (>= (length lists) 2)
Known issues:
Postcondition contract checking will not operate on functions returning multiple values. If the postcondition is omitted then the multiple values will be returned as normal. Precondition contracts are not affected.
Define a top-level function binding as with define's "defun"
syntax, with the addition of precondition and/or postcondition contracts.
The semantics of the pre- and post-conditions is equivalent to
define-lambda.
Example:
(define-contract (add-map . lists)
(pre (every list? lists)
(>= (length lists) 2)
(apply = (map length lists)))
(post list?
(lambda (ret) (= (length ret) (length (car lists)))))
(apply map + lists))
is equivalent to:
(define add-map
(lambda-contract lists
(pre (every list? lists)
(>= (length lists) 2)
(apply = (map length lists)))
(post list?
(lambda (ret) (= (length ret) (length (car lists)))))
(apply map + lists)))Known issues:
Binding to a lambda expression instead of using the "defun"
syntax breaks contract checking. Use a plain define with
lambda-contract instead.
See lambda-contract for issues with the contract system in
general.