Preconditions and Postconditions

Contract programming

Contract programming is very effective for reducing coding errors. You have seen two of the contract programming features earlier in the contract programming chapter: The in and out blocks ensure input and output contracts of functions.

Note: It is very important that you consider the guidelines under the in blocks versus enforce checks section of that chapter. The examples in this chapter are based on the assumption that problems with object and parameter consistencies are due to programmer errors. Otherwise, you should use enforce checks inside function bodies.

As a reminder, let’s write a function that calculates the area of a triangle by Heron’s formula. We will soon move the in and out blocks of this function to the constructor of a struct.

For this calculation to work correctly:

• The length of every side of the triangle must be greater than zero.

• Additionally, since it is impossible to have a triangle where one of the sides is greater than the sum of the other two, that condition must also be checked.

Once these input conditions are satisfied, the area of the triangle would be greater than zero. The following function ensures that all of these requirements are satisfied: