Using Assertions for Design by Contract

Design by Contract (DBC) is a concept developed by Bertrand Meyer, creator of the Eiffel programming language, to help in the creation of robust programs by guaranteeing that objects follow certain rules that cannot be verified by compile-time type checking.^[93] These rules are determined by the nature of the problem that is being solved, which is outside the scope of what the compiler can know about and test.

Although assertions do not directly implement DBC (as does the Eiffel language), they can be used to create an informal style of DBC programming.

The fundamental idea of DBC is that a clearly-specified contract exists between the supplier of a service and the consumer or client of that service. In object-oriented programming, services are usually supplied by objects, and the boundary of the object—the division between the supplier and consumer—is the interface of the object’s class. When clients call a particular public method, they are expecting certain behavior from that call: a state change in the object, and a predictable return value. Meyer’s thesis is that:

1. This behavior can be clearly specified, as if it were a contract.
2. This behavior can be guaranteed by implementing certain run-time checks, which he calls preconditions, postconditions and invariants.

Whether or not you agree that point 1 is always true, it does appear to be true for enough situations to make DBC an interesting approach. (I believe that, like any solution, there are boundaries to its usefulness. But if you know these boundaries, you know when to try to apply it.) In particular, a very valuable part of the design process is the expression of the DBC constraints for a particular class; if you are unable to specify the constraints, you probably don’t know enough about what you’re trying to build.

Check instructions

Before going into in-depth DBC facilities, consider the simplest use for assertions, which Meyer calls the check instruction. A check instruction expresses your conviction that a particular property will be satisfied at this point in your code. The idea of the check instruction is to express non-obvious conclusions in code, not only to verify the test, but also as documentation to future readers of the code.

For example, in a chemistry process, you may be titrating one clear liquid into another, and when you reach a certain point, everything turns blue. This is not obvious from the color of the two liquids; it is part of a complex reaction. A useful check instruction at the completion of the titration process would assert that the resulting liquid is blue.

Another example is the Thread.holdsLock( ) method introduced in JDK 1.4. This is used for complex threading situations (such as iterating through a collection in a thread-safe way) where you must rely on the client programmer or another class in your system using the library properly, rather than on the synchronized keyword alone. To ensure that the code is properly following the dictates of your library design, you can assert that the current thread does indeed hold the lock:

assert Thread.holdsLock(this); // lock-status assertion

Check instructions are a valuable addition to your code. Since assertions can be disabled, check instructions should be used whenever you have non-obvious knowledge about the state of your object or program.

Preconditions

A precondition is a test to make sure that the client (the code calling this method) has fulfilled its part of the contract. This almost always means checking the arguments at the very beginning of a method call (before you do anything else in that method) to make sure that those arguments are appropriate for use in the method. Since you never know what a client is going to hand you, precondition checks are always a good idea.

Postconditions

A postcondition test checks the results of what you did in the method. This code is placed at the end of the method call, before the return statement, if there is one. For long, complex methods where the result of the calculations should be verified before returning them (that is, in situations where for some reason you cannot always trust the results), postcondition checks are essential, but any time you can describe constraints on the result of the method, it’s wise to express those constraints in code as a postcondition. In Java these are coded as assertions, but the assertion statements will vary from one method to another.

Invariants

An invariant gives guarantees about the state of the object that will be maintained between method calls. However, it doesn’t restrain a method from temporarily diverging from those guarantees during the execution of the method. It just says that the state information of the object will always obey these rules:

1. Upon entry to the method.
2. Before leaving the method.

In addition, the invariant is a guarantee about the state of the object after construction.

According to the this description, an effective invariant would be defined as a method, probably named invariant( ), which would be invoked after construction, and at the beginning and end of each method. The method could be invoked as:

assert invariant();

This way, if you chose to disable assertions for performance reasons, there would be no overhead at all.

Relaxing DBC

Although he emphasizes the importance of being able to express preconditions, postconditions, and invariants, and the value of using these during development, Meyer admits that it is not always practical to include all DBC code in a shipping product. You may relax DBC checking based on the amount of trust you can place in the code at a particular point. Here is the order of relaxation, from safest to least safe:

1. The invariant check at the beginning of each method may be disabled first, since the invariant check at the end of each method will guarantee that the object’s state will be valid at the beginning of every method call. That is, you can generally trust that the state of the object will not change between method calls. This one is such a safe assumption that you might choose to write code with invariant checks only at the end.
2. The postcondition check may be disabled next, if you have reasonable unit testing that verifies that your methods are returning appropriate values. Since the invariant check is watching the state of the object, the postcondition check is only validating the results of the calculation during the method, and therefore may be discarded in favor of unit testing. The unit testing will not be as safe as a run-time postcondition check, but it may be enough, especially if you have enough confidence in the code.
3. The invariant check at the end of a method call may be disabled if you have enough certainty that the method body does not put the object into an invalid state. It may be possible to verify this with white-box unit testing (that is, unit tests that have access to private fields, so they may validate the object state). Thus, although it may not be quite as robust as calls to invariant( ), it is possible to “migrate” the invariant checking from run-time tests to build-time tests (via unit testing), just as with postconditions.
4. Finally, as a last resort you may disable precondition checks. This is the least safe and least advisable thing to do, because although you know and have control over your own code, you have no control over what arguments the client may pass to a method. However, in a situation where (a) performance is desperately needed and profiling has pointed at precondition checks as a bottleneck and (b) you have some kind of reasonable assurance that the client will not violate preconditions (as in the case where you’ve written the client code yourself) it may be acceptable to disable precondition checks.