Benefits of using 'Design by Contract'

Question

I am studying the 'Design by Contract' development methodology. However, I am having a hard time seeing its advantages.

For example, it is said that one of the characteristics of this methodology is that the preconditions of a function can be expressed in its header. Thus, we could have this example, in which we divide the number 10 by any number whose precondition is that it must be greater than 0:

 get_result(value:INTEGER): REAL is require valid_value: value > 0 do Result := 10 / value ensure Result = 10 / value end

However, what benefit does it give me compared to this other more traditional way of doing it?

get_result(value:INTEGER): REAL is do if value>0 Result := 10 / value else --throw an exception: throw valid_value_exception end end

What I'm seeing is that the only thing that changes between the two ways of doing it is the site where the preconditions are validated. In the first form, the precondition is validated in the header of the function, while in the second form, the precondition is evaluated in the body of the function, but, in both cases, you have to continue doing the validations.

I'm sure I'm missing something important. I would appreciate if someone could help me on this.

Alexander Kogtenkov · Accepted Answer · 2021-05-12 15:53:44Z

The key property of the Design by Contract methodology is that a correct program behaves exactly the same when assertions are monitored and when they are not. In other words, in a correct program assertion monitoring can be turned off without affecting the program behavior.

Assertion monitoring can be turned off after making sure all required tests pass (an unsound approach) or by using a verification tool that checks assertions at compile time rather than at run time (the example is written in Eiffel, the corresponding verification tool is AutoProof; other languages with design-by-contract support have other similar tools).

Whereas the requirement that the argument should be above zero could be documented in the description of the feature, comments (usually) are not consumable by programming language tools like compilers, code analyzers, etc., and could not be used for program verification, automatic test generation and other automated tasks.

Preconditions and postconditions also play a role in responsibility separation. Preconditions allow the supplier to rely on the guarantees provided by the client. Postconditions allow the client to rely on the guarantees provided by the supplier. Note that in both cases there is no need to repeat the checks and no need to catch exceptions or to check the result. All the knowledge is accumulated in the associated assertions. Were the checks done inside the method body, in the implementation part, there would be no glue what was guaranteed, what result was expected, etc.

Use of both preconditions and postconditions enables chaining the calls. Let's consider an expression

get_result ((get_result (n * n + 1).ceiling)

The precondition of the first feature call is satisfied by construction. Its postcondition guarantees that the result is a positive value. The call to ceiling makes sure the argument to the outer feature satisfies its precondition. So we can prove that the expression never throws an exception without ever looking into the implementation of get_result (provided that it is correct). In fact, several implementations are possible, but we do not care which implementation is used.

To summarize, preconditions and postconditions

can be turned off at run-time for correct programs
are consumable by program analysis tools
are used to verify programs at compile time (and make this verification modular)
separate responsibilities between client and supplier (who is guilty of a bug?)
remove the need for additional checks at the client side thus simplifying feature call chaining

Thanks for the elaborate response and for your time, @alexander-kogtenkov. More doubts have arisen in the wake of what you have stated. Would you be so kind as to be able to solve them?
1. Says the following: "The key property of the Design by Contract methodology is that a correct program behaves exactly the same when assertions are monitored and when they are not." When you mention 'assertions', are you referring to preconditions and postconditions?
3. When you say: "Assertion monitoring can be turned off after making sure all required tests pass (an unsound approach) or by using a verification tool that checks assertions at compile time rather than at run time."
You say that checking assertions at compile time using verification tools is a better approach than testing. What I don't understand at this point is how, at compile time, you can check that the preconditions and postconditions are met. Imagine, for example, the case of a client who calls the supplier's method (whose precondition is that the number that the client passes to him is greater than zero). In case the number passed by the client is dynamically generated (for example, by keyboard input by the user), how can you know at compile time that this condition is met?
4. Is this methodology appropriate for all types of projects or is it intended only for a specific type of project? For example, if my project does not use any external API and is only based on the methods implemented in my project, would it be appropriate to specify in all the methods the preconditions and the postconditions?

Collectives™ on Stack Overflow

Benefits of using 'Design by Contract'

1 Answer 1

23 Comments

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

23 Comments

Related