JML

JML, which stands for Java Modeling Language, is a specification language for Java. JML can be used to to specify the behaviour and detailed design of Java programs, by adding annotations to Java source files. These annotations can for instance be preconditions, postconditions, or invariants, in the Design-by-Contract style of Eiffel, but JML specifications can be much more precise and complete than those typically given in Eiffel.

The aim of JML is to provide a specification language that is easy to use for Java programmers and that is supported by a wide range of tools for specification type-checking, runtime debugging, static analysis, and verification. An overview of all the tools that currently support JML is given here. One of these tools is the LOOP tool developed in the SoS group in Nijmegen, which allows at program verification for JML-annotated Java programs.

   interface Account {
     //@ public model int balance;
     //@ invariant balance >= 0;

     /*@  requires   m >= 0;
       @  assignable balance;
       @  ensures    balance == \old(balance) + m;
       @*/
     void credit(int m);

     /*@ normal_behavior
       @   requires   balance >= m && m >= 0;
       @   assignable balance;
       @   ensures    balance == \old(balance) - m;
       @ also
       @ exceptional_behavior
       @   requires   balance < m;
       @   signals    (AccountException e) e.getMessage().equals("INSUFFICIENT FUNDS");
       @*/
     void debit(int m);
   }

The initiative in the development of JML was taken by Gary Leavens at Iowa State University, but the development of JML and tools for JML has grown into a cooperative, open effort, involving many people world-wide.

The SoS group is involved in the language design, semantics, and the proof theory of JML. See also our work on an ESC/Java 2, an open source version of the static checker for Java. We are also actively using JML for the specification of real Java programs; here the focus is on Java Card programs for smart cards. JavaCard, a stripped-down version of Java for programming smart cards. In particular, we have written a formal specification of the Java Card API in JML, which can be downloaded here.

For more information, contact Erik Poll.