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