From C2:
Design By Contract (DbC) is a software correctness methodology. It uses preconditions and postconditions to document (or programmatically assert) the change in state caused by a piece of a program. Design by Contract is a trademarked term of Bertrand Meyer and implemented in his Eiffel? Language as assertions.
In short, you use precondition, and postcondition testing to ensure that calls to, and values returned from your functions are consistent and correct.
The typical name for the precondition check is require. ensure is the name of the postcondition check. There is also the invariant check which states an eternal truth. The invariant may become false during the execution of a function, but it must be true on entry, and exit.
Thanks for catching that Greg. I fixed the definition. When it comes to invariants in scheme, surely invariants are applicable in a closure. Assume we have a special form invariant consider:
(define (make-cheese-ball-closure-invariant-example some-bar)
(let ((my-invariant-related-var 0))
(lambda (foo)
(do (some-stuff (with (and foo some-bar)
my-invariant-related-var)))
(invariant (> my-invariant-related-var 23)))))
In plt-scheme there is a package available. Some details are here: http://www.cs.utah.edu/plt/mailarch/plt-scheme-2002/msg00846.html.
Writing your own DbC system would not be that difficult. See this C implementation using macros, and this CommonLisp implementation.
I believe the above definition of an invariant is incorrect. It can become false during the execution of a function, but must be true both before and after the function. The invariant is (I think) limited to OO DbC -- it asserts some quality about the class as a whole, and so must be checked before and after every function call.
I suppose invariants could be used outside classes, but they would be effectively global ... needing to be checked before and after every method call in the system. That's pretty gnarly.