This chapter is from the book
This chapter is from the book
This chapter is from the book
1.7 Trustworthy Documentation
In the previous section, we saw that contracts can be checked at runtime, delivering valuable debugging information. We took an example of a faulty caller who broke a precondition. What if the component itself contains a bug? Then a postcondition (or the invariant) will evaluate to false, highlighting the problem and its cause.
For example, suppose that the developer of the component forgot to increment the count in the feature to add a new customer. During testing, the add feature is called. Its postcondition is evaluated. And up comes a message, like the one in the previous section, telling the developer that the false postcondition was the one with the tag count_increased in the add feature in the CUSTOMER_ MANAGER class.
If an application survives execution without any false preconditions, postconditions, or invariants, we can be sure that the code is doing what the contract says.
Now turn that around. By checking that the code is doing what the contract says, the runtime system is also checking that the documentation accurately says what the code does. If one assertion in the contract did not correctly describe what the code did, that assertion would evaluate to false on some test.
In other words, if you document your classes using contracts, you get documentation that everyone can trust to be telling the truth. There's a novelty!
Further, the documentation sets out clearly the rights and obligations of each party to the contract. In any one call to a feature, one object will be playing the role of client, or caller. The other will be playing the role of supplier.
A client calling a feature on a supplier has an obligation to fulfill the precondition. A client who calls a feature when its precondition is false has broken the client's side of the contract. The supplier's called feature has an obligation to terminate with the postcondition true. A feature that leaves its postcondition false has broken the supplier's side of the contract.
In return for these obligations, both parties obtain rights. The client has the right to expect that the called feature makes its postcondition true. If the postcondition is false, this is not the fault of the client. The supplier has the right to expect that the precondition is true. If the feature is called with the precondition false, this is not the fault of the supplier, which is then not obliged to meet its postcondition.
There is more on this theme in Chapter 8.