Dr. Dobb's Journal November 1998

GEF and Programming by Contract

Eiffel is a programming language that champions the "programming by contract" paradigm, an alternate approach for dealing with exceptional conditions. In such a paradigm, your function specifies the specific conditions, in the form of assertions, that must hold true before a client may execute your function. In addition, your function may also specify any conditions that must hold true after it completes its operation.

For example, a function that computes the square root of a number may require that its input be nonnegative. This is a precondition. In addition, the function may, as part of its contract, guarantee that the absolute value of the difference between the number and the square of the answer not exceed 0.0001. This is a postcondition.

Another aspect of a contract is the invariant -- a condition that must be true at the beginning of a function's execution and hold true after it returns, as well.

For example, imagine that you created a dynamic array data structure in C, whose lower and upper bounds could change dynamically, increasing or decreasing, depending upon whether you added elements to the top of the array, or to the bottom of the array, or removed elements from the top of the array, or from the bottom. A condition that would always hold true, regardless of the operation, is that the upper bound of the array minus its lower bound plus 1 would always be equal to its size. This is an invariant. For example, an array whose size is 0 might have a lower bound of 0 and an upper bound of -1. This would satisfy the invariant, since the upper bound, -1, minus the lower bound, 0, plus 1 would be equal to the size of the array, 0. The existence of invariant, precondition, and postcondition statements can make your program very robust.

-- B.B.

Back to Article