Coryoth's Journal: Better Programming in Java

Sometimes ideas don't get the attention that they deserve. The Java Modelling Language (JML) is just such an idea. JML is something every Java programmer should know about. That does not mean every project in Java should make use of JML, only that developers should be aware of it so they can use it wherever it does make sense. The fact is that JML provides so many benefits for so little extra work that it deserves far more use than it gets. If you program in Java it could make your life a lot easier.

What is JML?

In a sense JML is just a way to document your code better. JML provides simple intuitive syntax to provide concise descriptions of behaviour in a Java module. JML uses annotations to document all the mundane things you would normally document. For example you might want to note which fields are allowed to ever be null, or whether a particular method requires one of its parameters to be greater than zero, or if a method is side-effect free. What JML really offers, however, is the tools to make use of these extra comments to save you time and effort later. JML simply asks you to do what you would normally do, and in return offers improved productivity when it comes to documenting, testing, and debugging your code.

So what exactly does JML look like? Here's a simple toy example that, while contrived, manages to demonstrate a lot of basic JML and will be useful later for demonstrating what tools that use JML can do.

public class Example {
 
    public int modifiable = 0;
    private /*@ spec_public @*/int additional_value = 5;
    private /*@ spec_public non_null @*/ String current_substring;
 
//@ invariant additional_value >= 5;
//@ invariant current_substring.length() == modifiable;
 
//@ requires ((String) o).length() > modifiable;
//@ assignable current_substring;
    public void castExample(/*@ non_null @*/ Object o) {
        additional_value = o.hashCode()%5;
        current_substring = ((String) o).substring(0, modifiable);
    }
 
//@ requires x >= -5;
//@ ensures \result > 0;
    public /*@ pure @*/ int pureFunction(int x) {
        return x + additional_value;
    }
 
//@ assignable modifiable;
//@ signals (ExampleException e) additional_value <= 4;
    public void unreachable() throws ExampleException {
        if (additional_value > 4 && modifiable > 0) {
            modifiable++;
        }
        else if (modifiable == 0) {
            throw new ExampleException();
        }
        else {
//@ unreachable;
        }
    }
}

Most of the JML annotations should be clear: We are simply documenting constraints on inputs (requires clauses) and outputs (ensures clauses, noting when fields or parameters cannot be null or when code is (we presume) unreachable, and what invariant properties that we expect the objects to have. A little less immediately obvious are the assignable and signals clauses. An assignable clause declares what is allowed to be written/assigned to from within the method, and a signals clause declares conditions that must be met in the case of an exception being thrown. Finally spec_public simply declares that these private fields have public visibility to the specification. You may note a few errors where the specification and the code don't agree - we'll come to those shortly.

This is, of course, only a small sample of what JML offers. JML provides a lot of useful syntactic sugar to make stating your intentions as easy and natural as possible. For a proper introduction to JML there are some presentations on basic JML and more advanced JML. Full documentation can be found in the JML Reference Manual.

What do I get out of it?

JML provides an easy to use language with which you can concisely say how you intend your code to behave. More importantly it provides tools to make full use of that. For the small amount of extra effort of documenting your intentions with JML you get a lot of easy gains.

The JML tools

The JML distribution comes with a number of tools that use JML annotations. The four most useful are jmldoc, jmlc, jmlrac, and jmlunit. The first, jmldoc performs the same function as Javadoc, producing almost identical API documentation. The advantage of jmldoc is that it understands JML annotations and includes suitable extra information in the API documents based on the annotations. As long as you document requirements and guarantees for modules in JML you can be sure that the API documentation will always include those constraints. Furthermore because JML annotations become integral for testing and debugging it is far more likely that the annotations are kept up to date with the code, meaning that documentation is also more likely to be up to date.

The tools jmlc and jmlrac provide a JML aware compiler and runtime environment. The advantage of compiling and running code with such tools is that JML annotations are converted into assertions which are checked at runtime, making it easier and faster to discover and locate bugs. For the small cost of writing a few annotations you can significantly speed up the testing and debugging cycle.

You can get the similar results by liberally sprinkling assertions through your code, but JML offers several advantages over such a scheme:

1. JML provides a lot of syntactic sugar like universal and existential quantifiers (\forall and \exists), and logical connectives like "implies" (==> ) and "if and only if" ().
2. JML elegantly handles inheritance. When overriding a method you will have to rewrite all your assertions, while JML annotations are automatically inherited. If you want to add annotations to those inherited by an overridden method JML provides the also keyword.
3. As JML annotations are comments, and only converted into runtime assertions when you use the jmlc compiler, turning off runtime checking is as easy as compiling with a standard Java compiler. Using assertions will have you jumping through hoops to arrange anything similar.
4. JML annotations can be automatically included into your JavaDoc documentation. If you use assertions you'll have to repeat the information elsewhere to get it included in the documentation

Of course having assertions based on intended behaviour is no substitute for a decent unit testing framework. JML has an answer for this too however. The jmlunit tool can read a Java module with JML annotations and automatically generate a JUnit test class based on the annotations. For example running jmlunit over our example above creates two new files Example_JML_Test.java and Example_JML_TestData.java. The first of those files is a JUnit test suite, and the second is used to generate test data. JML attempts to come up with a reasonable test data generation strategy, but leaves space for you to enter your own set of test data instead should you prefer.

Extended Static Checking

Extended static checking is where JML annotations begin to truly come into their own. ESC/Java2 is an extended static checking tool for Java that uses JML annotations to catch errors before you even compile, let alone run, the code. You can think of it as type checking on steroids - using the information in the annotations to warn you about a wide variety of potential errors. It runs about as fast as compilation, so there's no waiting for results.

Consider what happens when we run the example above through ESC/Java2. We get a series of warnings (some not revealed until others have been corrected):

1. We are warned that current_substring is uninitialized and could be null
2. We are warned that additional_value is modified when it shouldn't be (line 14)
3. We are warned that the cast made in castExample may be invalid
4. We are warned that the postcondition for pureFunction may be violated (it's possible that x = -5 while the invariant only ensures that additional_value is at least 5, thus 0 could be returned).
5. We are warned that an exception may be thrown in unreachable without the conditions being met
6. We are warned that the //@ unreachable portion of code is, in fact, reachable
7. We are warned that the invariant current_substring.length() == modifiable can be violated.

Most of the errors listed above are either errors in code, or in our expectations of what the code will do. Some of these errors can be remedied by strengthening the constraints. For example we can add //@ requires o instanceof String to castExample to fix the warning, but at the cost that any code calling that method must meet that precondition (though the API documentation will state the precondition). Other errors can only be corrected in the code itself.

While the errors are necessarily simple in this toy example, hopefully this gives you the flavour of what ESC/Java2 can do for you - it has very powerful algorithms and scales to remarkably complex code, easily finding errors that would be hard to spot by inspection. For more examples of what ESC/Java2 can do for you (and it is well worth reading) try this introduction to ESC/Java2. ESC/Java2 offers a robust and powerful tool for finding subtle errors in your code earlier when they are easier to fix.

Conclusions

JML is simple to use: it has an expressive and intuitive syntax, and you can write the annotations at the same time the code. JML is also flexible: you an use as much or as little in the way of annotations as you need. Perhaps you simply want to add some pre- and post-conditions, or just keep track of which methods can access or alter certain fields; perhaps you want to use the full power of the theorem provers in ESC/Java2. Most of all JML makes many aspects of development, from debugging and testing to documenting, easier and more efficient, all for very little extra effort. If you program in Java for a living then JML can almost certainly make your code better, and your life easier.