Java Modeling Language

El Java Modeling Language, abreviado JML y en español «Lenguaje de Modelaje para Java» es un lenguaje de especificación para programas Java, que se sirve de pre-, postcondiciones e invariantes de la lógica de Hoare, siguiendo el paradigma de diseño por contrato. Las especificaciones se escriben como comentarios de anotación Java en el código fuente, que por consiguiente puede compilarse con cualquier compilador de Java.

Para facilitar el desarrollo existen varias herramientas de verificación, tales como programas que chequean el código antes de su ejecución (ej. ESC/Java).

Generalidades

JML es un lenguaje de especificación de interfaz de comportamiento para módulos Java. JML provee una semántica para describir de forma formal el comportamiento de un módulo de Java, evitando así la ambigüedad con respecto a las intenciones del diseñador del módulo. JML ha heredado ideas de Eiffel, Larch y del cálculo de refinamiento, con la meta de proveer una semántica formal rigurosa a la vez que se hace accesible a todo programador de Java. Hay varias herramientas que se sirven de las especificaciones de comportamiento del JML. Dado que las especificaciones se pueden escribir como anotaciones en los archivos de programa de Java, o grabarse en otros archivos de especificación independientes. Los módulos de Java con las especificaciones JML se pueden compilar sin necesidad de cambio alguno con el compilador de Java.

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:

requires 

Define una precondición en el método que le sigue.

ensures 

Define una postcondición en el método que le sigue.

signals 

Define una postcondición para cuando se lanza una excepción por el método que le sigue.

signals_only 

Define que excepciones pueden ser lanzadas cuando cuando se da la precondición declarada.

assignable 

Define que campos están permitidos para ser asignados por el método que le sigue.

pure 

Declara un método libre de efectos colaterales (assignable \nothing).

invariant 

Define una propiedad invariante de la clase.

also 

Combina casos de especificación y también puede declarar que un método esta heredando especificaciones de sus supertipos.

assert 

Define una aserción JML.

spec_public 

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:

\result 

Un identificador para el valor de retorno de el método que le sigue.

\old(<expression>) 

Un modificador para referirse al valor de la <expression> en el momento de entrada en un método.

(\forall <decl>; <range-exp>; <body-exp>) 

El cuantificador universal.

(\exists <decl>; <range-exp>; <body-exp>) 

El cuantificador existential.

a ==> b 

a implica b

a <== b 

a está implicado por b

a <==> b 

a sólo si b

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 Manual de referencia de JML.

Herramientas de soporte

Una serie de herramientas proveen funcionalidad basada en las anotaciones JML. Las herramientas de la Iowa State JML otorgan un compilador que verifica las aserciones jmlc que convierte las anotaciones JML en aserciones de tiempo de ejecución, un generador de documentos jmldoc que produce documentación Javadoc ampliada con información extra de las anotaciones JML y un generador de tests de módulos jmlunit que genera un marco para tests JUnit a partir de las anotaciones JML.

También hay grupos independientes que trabajan en herramientas que hacen uso de las anotaciones JML, entre ellas:

• ESC/Java2 [1], un verificador estático extendido que utiliza anotaciones JML;
• Daikon, un generador invariante dinámico;
• KeY, que provee un comprobador de teorema con una fachada JML;
• Krakatoa, una herramienta de verificación estática basada en la plataforma de verificación Why y utilizando el asistente de evidencia Coq;
• JMLeclipse, un plugin para el IDE Eclipse con soporte de sintaxis JML e interfaces a varias herramientas que utilizan anotaciones JML.
• Sireum/Kiasan, un analizador estático basado en una ejecución simbólica que soporta JML como lenguaje de contrato.
• JMLUnit, una herramienta que genera archivos para ejecutar tests JUnit sobre archivos Java con anotación JML.
• TACO, programa de análisis de código abierto que estáticamente comprueba el cumplimiento de un programa de Java frente a su especificación en JML.

Referencias

• 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

Enlaces externos

• Página web de JML