Basic JML syntax provides the following keywords
- requires
- Defines a precondition on the method that follows.
- ensures
- Defines a postcondition on the method that follows.
- signals
- Defines a postcondition for when a given Exception is thrown by the method that follows.
- signals_only
- Defines what exceptions may be thrown when the given precondition holds.
- assignable
- Defines which fields are allowed to be assigned to by the method that follows.
- pure
- Declares a method to be side effect free (like assignable \nothing but can also throw exceptions). Furthermore, a pure method is supposed to always either terminate normally or throw an exception.
- invariant
- Defines an invariant property of the class.
- loop_invariant
- Defines a loop invariant for a loop.
- also
- Combines specification cases and can also declare that a method is inheriting specifications from its supertypes.
- assert
- Defines a JML assertion.
- spec_public
- Declares a protected or private variable public for specification purposes.
Basic JML also provides the following expressions
- \result
- An identifier for the return value of the method that follows.
- \old(<expression>)
- A modifier to refer to the value of the <expression> at the time of entry into a method.
- (\forall <decl>; <range-exp>; <body-exp>)
- The universal quantifier.
- (\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
= 0 && balance <= MAX_BALANCE;\n \n //@ assignable balance;\n //@ ensures balance == 0;\n public BankingExample() {\n this.balance = 0;\n }\n \n //@ requires 0 < amount && amount + balance < MAX_BALANCE;\n //@ assignable balance;\n //@ ensures balance == \\old(balance) + amount;\n public void credit(final int amount) {\n this.balance += amount;\n }\n \n //@ requires 0 < amount && amount <= balance;\n //@ assignable balance;\n //@ ensures balance == \\old(balance) - amount;\n public void debit(final int amount) {\n this.balance -= amount;\n }\n \n //@ ensures isLocked == true;\n public void lockAccount() {\n this.isLocked = true;\n }\n \n //@ requires !isLocked;\n //@ ensures \\result == balance;\n //@ also\n //@ requires isLocked;\n //@ signals_only BankingException;\n public /*@ pure @*/ int getBalance() throws BankingException {\n if (!this.isLocked) {\n return this.balance;\n } else {\n throw new BankingException();\n }\n }\n}\n"}}'>publicclass BankingExample{
publicstaticfinalintMAX_BALANCE=1000;
private/*@ spec_public @*/intbalance;
private/*@ spec_public @*/booleanisLocked=false;
//@ public invariant balance >= 0 && balance <= MAX_BALANCE;
//@ assignable balance;
//@ ensures balance == 0;
publicBankingExample(){
this.balance=0;
}
//@ requires 0 < amount && amount + balance < MAX_BALANCE;
//@ assignable balance;
//@ ensures balance == \old(balance) + amount;
publicvoidcredit(finalintamount){
this.balance+=amount;
}
//@ requires 0 < amount && amount <= balance;
//@ assignable balance;
//@ ensures balance == \old(balance) - amount;
publicvoiddebit(finalintamount){
this.balance-=amount;
}
//@ ensures isLocked == true;
publicvoidlockAccount(){
this.isLocked=true;
}
//@ requires !isLocked;
//@ ensures \result == balance;
//@ also
//@ requires isLocked;
//@ signals_only BankingException;
public/*@ pure @*/intgetBalance()throwsBankingException{
if(!this.isLocked){
returnthis.balance;
}else{
thrownewBankingException();
}
}
}
Full documentation of JML syntax is available in the JML Reference Manual.
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 Archived 2005-12-11 at the Wayback Machine, 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 JML.
- Krakatoa Archived 2009-05-08 at the Wayback Machine, a static verification tool based on the Why verification platform and using the Rocq proof assistant.
- JMLEclipse, a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.
- Sireum/Kiasan, a symbolic execution based static analyzer which supports JML as a contract language.
- JMLUnit, a tool to generate files for running JUnit tests on JML annotated Java files.
- TACO, an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.
- Gary T. Leavens and Yoonsik Cheon. Design by Contract with JML; Draft tutorial.
- Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design; in Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, Kluwer, 1999, chapter 12, pages 175-188.
- Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), September 2009. HTML
- Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. Formal specification with JML. 2014. download (CC-BY-NC-ND)