(nytpu contracts)

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.

lambda-contract

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

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.