Design by contract and assert statements

Question

I am interested in the Design by Contract approach. It seems that for preconditions checked exceptions must be used to enforce them.
But for post-conditions and class-invariants I think that assertions are preferred.
Am I right? If I am correct, why for post-conditions and class-invariants assertions which may be disabled are allowed? Shouldn't post-conditions and invariants also be enforced?

Answer 1

Post conditions and class invariants on a component can only fail if the component itself is written incorrectly. Unit tests should catch all of these. It's permissible, of course, to actually check them in production, but this isn't necessarily worth the performance tradeoff.

On the other hand, preconditions can fail if the users of that component are incorrect. Tests on the component itself cannot check these, so it's necessary to fail more actively so that those unit tests fail.

Answer 2

Violating a precondition is by definition a programming error. It is therefore most unfortunate to signal such a violation with checked exceptions. Because code that is correct will be forced to explicitly catch an exception that certainly will never be thrown, and rethrow it as an unchecked exception, so that the programming error may be detected.

Answer 3

You should not be treating them differently - they should all be assertions.

OP says:

... It seems that for preconditions checked exceptions must be used to enforce them. ... why for post-conditions and class-invariants assertions which may be disabled are allowed? Shouldn't post-conditions and invariants also be enforced?

You seem to suggest that pre-conditions, post-conditions, and class-invariants should be always-on and always checked by the service (method/callee). If we're talking about Design-by-Contract (DBC) that originated from Bertrand Meyer, then this is not so. Meyers contends that, from a production code perspective, these conditions should be ensured in only one place, either by the client (caller) or by the service (callee) - this is the contract between client and service. In contrast, defensive programming says you should code the check in both places (which Meyers considers wasteful and adds unnecessary complexity).

The contract part of DBC is that the specification will be clear who is responsible for what: if the client will ensure the pre-conditions (and the service can assume they will true), then the service will ensure the post-conditions (and the caller can assume they will be true). Meyers certainly understood that it is wise for the service to check the preconditions/post-conditions/invariants for testing and debugging purposes (to ensure that the system will fail fast during test/debug), which is why it is wise to assert these conditions and have assertions enable during test/debug, but the intention is that these checks can be disabled or removed for production.

For example, if you design a stack such that its the caller's responsibility to check that the stack is not empty before calling pop() (precondition), then you shouldn't also code into the pop() method as part of the production code a check that the stack is not empty nor should you have a checked exception as part of the method signature to handle the condition. Its okay to have the precondition assertion there to assist with validation and debugging, but the intent is that once the development and testing is done (the code presumably bug-free), the production code will run with only the caller ensuring the precondition, not the callee (if that is how you designed the contract for the API).

If you have a checked exception as part of the pop() method and you check whether the stack is empty in the pop() method as part of the always-on, must be handled, production code, then you are saying that the service (callee) is taking responsibility for the check and that it is promising to throw the exception if the stack is empty - it is now part of the postcondition. In that case, the caller's don't need to check it explicitly - they should just handle the exception. Otherwise, if both the caller and callee check whether the stack is empty first, then it isn't design-by-contract.

On final note, some people take this to mean that Meyer's says that the caller should always be responsible for checking the stack is not empty or that the parameters are not null, etc. Not so - Meyers only says that you must be clear in the spec about the preconditions and post-conditions so that the clients and service can be coded correctly. You as the API designer and implementor decide what's in the preconditions and post-conditions. If you can be reasonable sure that the clients (callers) will ensure the preconditions (e.g. because its an internal class and you control everywhere the service/method is called), then make the "stack-is-not-empty" or the "parameter-a-is-not-null" part of the precondition and put the onus on the client. However, if you don't think that is a reasonable assumption (e.g. its a public API or clients can't be reviewed or tested to ensure compliance) and the ramifications of failed preconditions are severe, then don't make those assumptions part of the precondition: go ahead and put the check in the service and make the checked exception part of the signature - make it part of the post-condition that if the stack is empty when pop() is called, then the service will throw the checked exception.

[[Sorry for the rant-like answer - I'm a big fan of Bertrand Meyer and Design-by-Contract.]]