Template:Computer Programming/Error Handling/6

As you see the function demands a precondition of X >= 0 - that is the function can only be called when X ≥ 0. In return the function promises as postcondition that the return value is also ≥ 0.

In a full DbC approach, the postcondition will state a relation that fully describes the value that results when running the function, something like result ≥ 0 and X = result * result. This postcondition is √'s part of the contract. The use of assertions, annotations, or a language's type system for expressing the precondition X >= 0 exhibits two important aspects of Design by Contract:

1. There can be ways for the compiler, or analysis tool, to help check the contracts. (Here for example, this is the case when X ≥ 0 follows from X's type, and √'s argument when called is of the same type, hence also ≥ 0.)
2. The precondition can be mechanically checked before the function is called.

The 1^st aspect adds to safety: No programmer is perfect. Each part of the contract that needs to be checked by the programmers themselves has a high probability for mistakes.

The 2^nd aspect is important for optimization — when the contract can be checked at compile time, no runtime check is needed. You might not have noticed but if you think about it: $A^{2}+B^{2}$ is never negative, provided the exponentiation operator and the addition operator work in the usual way.

We have made 5 nice error handling examples for a piece of code which never fails. And this is the great opportunity for controlling some runtime aspects of DbC: You can now safely turn checks off, and the code optimizer can omit the actual range checks.

DbC languages distinguish themselves on how they act in the face of a contract breach:

1. True DbC programming languages combine DbC with exception handling — raising an exception when a contract breach is detected at runtime, and providing the means to restart the failing routine or block in a known good state.
2. Static analysis tools check all contracts at analysis time and demand that the code written in such a way that no contract can ever be breached at runtime.