Edición de «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 (lenguaje de programación)|Java]], que se sirve de [[precondición|pre-]], [[postcondición|postcondiciones]] e [[invariante]]s 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 (lenguaje de programación)|Eiffel]], [[Larch family|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:

; <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].

== 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 <code>jmlc</code> que convierte las anotaciones JML en aserciones de [[tiempo de ejecución]], un generador de documentos <code>jmldoc</code> que produce documentación [[Javadoc]] ampliada con información extra de las anotaciones JML y un generador de tests de módulos <code>jmlunit</code> 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]] [https://web.archive.org/web/20110514011545/http://secure.ucd.ie/products/opensource/ESCJava2/], un verificador estático extendido que utiliza anotaciones JML;
* [http://pag.csail.mit.edu/daikon/ Daikon], un generador invariante dinámico;
* [[KeY]], que provee un comprobador de teorema con una fachada JML;
* [http://krakatoa.lri.fr/ Krakatoa], una herramienta de verificación estática basada en la plataforma de verificación [http://why.lri.fr/ Why] y utilizando el asistente de evidencia [[Coq]];
* [http://jmleclipse.projects.cis.ksu.edu/ JMLeclipse], un plugin para el [[Integrated Development Environment|IDE]] [[Eclipse (software)|Eclipse]] con soporte de sintaxis JML e interfaces a varias herramientas que utilizan anotaciones JML.
* [http://www.sireum.org/?q=node/21/ Sireum/Kiasan], un analizador estático basado en una ejecución simbólica que soporta JML como lenguaje de contrato.
* [https://www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlunit.html JMLUnit], una herramienta que genera archivos para ejecutar tests JUnit sobre archivos Java con anotación JML.
* [https://web.archive.org/web/20110706084805/http://www.dc.uba.ar/inv/grupos/rfm_folder/TACO 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. [http://www.jmlspecs.org/jmlrefman/jmlrefman_toc.html HTML]

== Enlaces externos ==
* [http://www.jmlspecs.org/ Página web de JML]

{{Control de autoridades}}
[[Categoría:Plataforma Java]]
[[Categoría:Lenguajes de especificación]]