JML: The good and the bad

Our most recent assignment was based on the design methodology design by contract. We were asked to use the Java modeling language (JML), an annotation based specification language for Java to ensure our programs were developed to specification.

Here are some interesting observations:

- The idea of JML is very good. Its a non-intrusive mechanism of testing code. The JML annotations can be added before or after the method is fleshed out. (although DBC advocates writing these assertions first)

Eg. JML assertions
//@ requires firstname != "";
//@ requires lastname != "";
//@ requires username != "" || username.length() >4;
//@ requires password != "" || username.length() >4;
//@ requires address != null;
//@ requires !(\exists Customer c; this.customerDB.contains(c);c.getUsername() == username);
//@
//@ ensures \result != null;
//@ ensures (\exists Customer c; this.customerDB.contains(c); c.getUsername() == username);
//@
public Customer addCustomer(String firstname, String lastname, String username, String password, Address address)

- Since these are annotations, it does not mess up and over complicate your methods.
- The syntax is fairly simple, anyone who knows Java can use it.
- Its lightweight and seems to combine well with JUnit.
- It would work well for projects with well defined design specifications. If the design spec clearly specifies the input parameters of each method and its return type, then these annotations can be added at the time of defining your method signatures (at design time).
- It ensures the "contract" is preserved with the use of pre and post conditions. It also ensures correctness is maintained with the use of invariants.
- I feel it actually can take out the customary housekeeping tasks of ensuring your input parameters are not null/empty.

Improvement Suggestions:

- The most important improvement, i believe, should be in their error messages. When a pre/post/invariant is violated the error that is displayed (a JML Exception) is quite cryptic.

Eg.
org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError: by method TaxiBooking.validateAddress regarding specifications at
File "TaxiBooking.java", line 129, character 28 when
'zipcode' is

This error is actually thrown when a precondition ensuring that the input zipcode parameter is not empty, is violated.
Looking at the error its quite difficult to understand which precondition was violated. Its up to the developer to display or throw an exception with a more meaningful message. Otherwise the software testers would not understand the results of the JML test and the JML tests would only be used by the developers.
- JML seems to be very feature rich. However figuring out all of its features and hunting down documentation to support that was very cumbersome. If they can improve on the documentation, moreover provide more examples, it would be very helpful.
- Better integration with IDE's. I did find an eclipse plug-in, however it was for an older version of eclipse which was not forward compatible.
- I did find it to be a little fussy when it comes to constructors. Perhaps i didn't use it correctly, but it complained when i simply instantiated an object and then used its setter methods to set its attributes. It worked fine when i passed all of its attributes in the constructor and then instantiated the object (which is quite messy in my opinion).

Overall i believe JML has the potential to become quite popular in the industry, provided the right support (IDE) and documentation is made available.