SE450: DBC: Pre/Post/Invariants [9/24] ![]() ![]() ![]() |
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.