views:

95

answers:

2

Let's assume I have the following code:

public class MainClass {
    public static void main(String[] args) {
        System.out.println(sumNumbers(10, 10));
    }

    //@requires a >= 10;
    //@ensures \result < 0;
    public static int sumNumbers(int a, int b) {
        return a+b;
    }
}

I can make 2 things here:

Use Code Contracts (in this case, what is in comments). When sumNumbers is run and a < 10, it will throw immediatly an exception (although it doesn't seem to be very descriptive):

Exception in thread "main" org.jmlspecs.jmlrac.runtime.JMLInternalNormalPostconditionError: by method MainClass.sumNumbers
    at MainClass.sumNumbers(MainClass.java:500)
    at MainClass.internal$main(MainClass.java:9)
    at MainClass.main(MainClass.java:286)

or...

Throw an exception. The exception can be as descriptive as I want. I'd also to check in the end of the function to see whenever the post conditions are true or not.

Which would you use here and why?

+1  A: 

Do you expect that invalid inputs might be passed to this argument during normal operation of your program? If they are, can you recover from it?

If so, checked exceptions are the way to go.

If you can't recover from this sort of case, then by all means make it a contract and fail loudly - but in either case I would use a descriptive error message.

danben
+2  A: 

I like the idea of the code contracts, but the descriptive IllegalArgumentException (or similar) tips it for me. It's much clearer in a support/production role (or even a development) to get an explicit exception message, which gives you a head start in diagnosis what's going wrong (whether a system is broken, or if you're misusing an API during development).

Brian Agnew
best idea: use both!
matt b
If you can, yes. I'm not familiar with 'code contracts' as presented above
Brian Agnew
There would be no point in using both. The idea of having a Code Contract stating that x >= 0 is that I don't have to check it again in the method body. So there is no point in using both.
devoured elysium