(\exists <decl>; <range-exp>; <body-exp>) The existential quantifier. a ==> b a implies b a <== b a is implied by b a <==> b a if and only if b as well as standard Java syntax for logical and, or, and not. JML annotations also have access to Java objects, object methods and operators that are within the scope of the method being annotated and that have appropriate visibility. These are combined to provide formal specifications of the properties of classes, fields and methods. For example, an annotated example of a simple banking class may look like public class BankingExample { public static final int MAX_BALANCE = 1000; private /*@ spec_public @*/ int balance; private /*@ spec_public @*/ boolean isLocked = false; //@ public invariant balance >= 0 && balance <= MAX_BALANCE; //@ assignable balance; //@ ensures balance == 0; public BankingExample() { this.balance = 0; } //@ requires 0 < amount && amount + balance < MAX_BALANCE; //@ assignable balance; //@ ensures balance == \old(balance) + amount; public void credit(final int amount) { this.balance += amount; } //@ requires 0 < amount && amount <= balance; //@ assignable balance; //@ ensures balance == \old(balance) - amount; public void debit(final int amount) { this.balance -= amount; } //@ ensures isLocked == true; public void lockAccount() { this.isLocked = true; } //@ requires !isLocked; //@ ensures \result == balance; //@ also //@ requires isLocked; //@ signals_only BankingException; public /*@ pure @*/ int getBalance() throws BankingException { if (!this.isLocked) { return this.balance; } else { throw new BankingException(); } } } Full documentation of JML syntax is available in the JML Reference Manual. Tool support A variety of tools provide functionality based on JML annotations. The Iowa State JML tools provide an assertion checking compiler jmlc which converts JML annotations into runtime assertions, a documentation generator jmldoc which produces Javadoc documentation augmented with extra information from JML annotations, and a unit test generator jmlunit which generates JUnit test code from JML annotations. Independent groups are working on tools that make use of JML annotations. These include: ESC/Java2 , an extended static checker which uses JML annotations to perform more rigorous static checking than is otherwise possible. OpenJML declares itself the successor of ESC/Java2. Daikon, a dynamic invariant generator. KeY, which provides an open source theorem prover with a JML front-end and an Eclipse plug-in (JML Editing) with support for syntax highlighting of