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?