Editando Java Modeling Language (sección)

== Sintaxis ==
Las especificaciones JML se agregan al código Java como anotaciones en los comentarios. Los comentarios Java se interpretan entonces como anotaciones JML cuando comienzan con el signo «@». Por ejemplo:

 //@ <especificación JML>

o

 /*@ <especificación JML> @*/

La sintaxis básica de JML cuenta con las siguientes palabras clave:

; <code>requires</code> : Define una [[precondición]] en el [[Método (informática)|método]] que le sigue.
; <code>ensures</code> : Define una [[postcondición]] en el método que le sigue.
; <code>signals</code> : Define una postcondición para cuando se lanza una [[Exception handling|excepción]] por el método que le sigue.
; <code>signals_only</code> : Define que excepciones pueden ser lanzadas cuando se da la precondición declarada.
; <code>assignable</code> : Define que campos están permitidos para ser asignados por el método que le sigue.
; <code>pure</code> : Declara un método libre de efectos colaterales (<code>assignable \nothing</code>).
; <code>invariant</code> : Define una [[Clase invariante|propiedad invariante de la clase]].
; <code>also</code> : Combina casos de especificación y también puede declarar que un método está heredando especificaciones de sus supertipos.
; <code>assert</code> : Define una [[aserción (informática)|aserción]] JML.
; <code>spec_public</code> : Declara una variable pública protegida o privada con el fin de una especificación.

El JML básico también provee las siguientes expresiones: 

; <code>\result</code> : Un identificador para el valor de retorno del método que le sigue.
; <code>\old(<expression>)</code> : Un modificador para referirse al valor de la <code><expression></code> en el momento de entrada en un método.
; <code>(\forall <decl>; <range-exp>; <body-exp>)</code> : El [[cuantificador universal]].
; <code>(\exists <decl>; <range-exp>; <body-exp>)</code> : El [[cuantificador existential]].
; <code>a ==> b</code> : <code>a</code> implica <code>b</code>
; <code>a <== b</code> : <code>a</code> está implicado por <code>b</code>
; <code>a <==> b</code> : <code>a</code> sólo si <code>b</code>

como cómo la [[sintaxis Java]] básica para lógica o para otros propósitos. Las anotaciones JML también tienen objeto a los objetos Java, los métodos de los objetos y operadores que están en el ámbito del método que se anota y que tienen una visibilidad adecuada. Estos se combinan para proveer especificaciones formales de las propiedades de las clases, campos y métodos. Por ejemplo, un ejemplo anotado de una sencilla clase de banco podrías ser así:

 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() { balance = 0; }
 
    //@ requires 0 < amount && amount + balance < MAX_BALANCE;
    //@ assignable balance;
    //@ ensures balance == \old(balance) + amount;
    public void credit(int amount) { balance += amount; }
 
    //@ requires 0 < amount && amount <= balance;
    //@ assignable balance;
    //@ ensures balance == \old(balance) - amount;
    public void debit(int amount) { balance -= amount; }
 
    //@ ensures isLocked == true;
    public void lockAccount() { isLocked = true; }
 
    //@   requires !isLocked;
    //@   ensures \result == balance;
    //@ also
    //@   requires isLocked;
    //@   signals_only BankingException;
    public /*@ pure @*/ int getBalance() throws BankingException {
        if (!isLocked) { return balance; }
        else { throw new BankingException(); }
    }
 }

La documentación íntegra sobre la sintaxis de JML se puede encontrar en el [http://jmlspecs.org/jmlrefman/jmlrefman_toc.html Manual de referencia de JML].