Archive for JML

The Java Modeling Language (JML)

Posted in Software Eng with tags , , on November 17, 2006 by wsjoung

JML makes it possible to specify the behavior of java modules. it combines the design by contract approach and the model-based specification approach. In another words, we can use JML to make strong the interface of java classes and easily checking return values.

Design by Contract with JML
Gary T. Leavens and Yoonsik Cheon (Jan 11, 2006)

There are two important check point, properties which are right before starting a method and properties which are right after finished a method including return value. We can catch those properties with requires clauses and ensures clauses.

//@ requires x >= 0.0;
/*@ ensures JMLDouble.approximatelyEqualTo(x, \result * \result, eps); @*/
public static double sqrt (double x) {
/* some codes. */
}

a requires clauses to specify the client’s obligation and an ensures clauses to specify the implementor’s obligation. A method’s precondition which is specified requires clauses says what must be true to call it. And, a method’s postcondition which is specified ensures clauses says what must be true when it terminates. Otherwise it throws an exception.

We also can define some contracts for not only methods but entire class.

/*@ public invariant !name.equals(“”)
@ && weight >= 0;
@*/

an invariant is a property that should hold in all client-visible states. It must be true when control is not inside the object’s methods. That is, invariant must hold at the end of each constructor’s execution, and at the beginning and end of all methods.

Formal documentation is another benefit of using JML. It makes more easier to read method’s behaviors.