# 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:
o
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 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 está 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 del 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í:
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 , 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.