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?

Pompey

A failed post condition would indicate a programming error that would be caught during development, when assertions are enabled- that's the only thing I can think of. using one or the other seems somewhat arbitrary. I would be more likely to use aspects anyway. – Sasaki

@DaveNewton:Won't aspects has a performance penalty? – Pompey

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.

Twitt

But calling methods and parameters, don't have side-effects on the class invariants?So why are they treated different than preconditions? – Pompey

If your code allows class invariants to fail under any circumstances, that's an error in your code. If your code is called with invalid inputs, that's an error in your caller's code. – Twitt

On the other hand, preconditions can fail if the users of that component are correct. Don't you mean incorrect? – Pompey

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.

Gerardgerardo

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. Meyer 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 Meyer considers wasteful and adds unnecessary complexity).

The contract part of DBC is that the specification will be clear on who is responsible for what: if the client will ensure the pre-conditions (and the service can assume they will be true), then the service will ensure the post-conditions (and the caller can assume they will be true). Meyer 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] 2 during test/debug), which is why it is wise to assert these conditions and have assertions enabled 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 it's 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. It's 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 whether the stack is not empty or that the parameters are not null, etc. Not so - Meyer 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. it's 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.]]

Erna