SE450: DBC: Pre/Post/Invariants [9/24] Previous pageContentsNext page

Assertions can be used to implement a design by contract style of programming. In Eiffel, this is done as part of the programming language itself. How do we do this in Java? What do we have at our disposal?

Preconditions

Postconditions

Invariants

Java offers us the following:

Preconditions - usually use exceptions, especially for public APIs. If your class is used by other classes (any arbitrary class), it should throw an exception if an argument is called that violates the contract).
However, if you are using exceptions (especially checked exceptions) in private code, this can be cumbersome. You may not want to have to put try-catch blocks in all of your private code (trusted). You may prefer to use assertions at this point, since the only code using your classes should be your own.

What can happen if you use assertions in a public API?


void command(Object o) {
    assert o != null;

    String s = o.toString();
}

Postconditions - use assert. You probably don't want to throw an exception after the completion of the code. You would prefer to do a check on some value, and assert that the assumption is true. If the contract is violated at this point, there is not much that can be done. By throwing exceptions, you are asking the client to attempt to recover from it.

Invariants - use assert. This is often part of the pre and post condition code, since it must be true at both times. Write an invariant method that can be called whenever a method is called and returns. This will ensure the class meets the invariant. The method should return a boolean.

Assertions a big part of iterative developement. They are similar to writing a unit test that will guarantee that if code changes to violate a contract, it will be caught. The difference is it is run every time the method is executed, allowing a more diverse set of test cases.

Previous pageContentsNext page