Java Modeling Language

Syntax

JML specifications are added to Java code in the form of annotations in comments. Java comments are interpreted as JML annotations when they begin with an @ sign. That is, comments of the form

//@

/*@ @*/

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 (this shorthand for assignable \nothing).
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(): A modifier to refer to the value of the at the time of entry into a method.
(\forall ; ; ): The universal quantifier.
(\exists ; ; ): 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.

Read more about this topic: Java Modeling Language

Java Modeling Language - Syntax