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?