Lenguaje de modelado Java

El lenguaje de modelado Java ( JML ) es un lenguaje de especificación para programas Java que utiliza precondiciones , postcondiciones e invariantes al estilo Hoare , siguiendo el paradigma de diseño por contrato . Las especificaciones se escriben como comentarios de anotación Java en los archivos fuente, que, por lo tanto, pueden compilarse con cualquier compilador Java .

Diversas herramientas de verificación, como un verificador de aserciones en tiempo de ejecución y el Verificador Estático Extendido ( ESC/Java ), facilitan el desarrollo.

JML es un lenguaje de especificación de interfaz de comportamiento para módulos Java. JML proporciona semántica para describir formalmente el comportamiento de un módulo Java, evitando ambigüedades respecto a las intenciones de sus diseñadores. JML hereda ideas de Eiffel , Larch y el Cálculo de Refinamiento , con el objetivo de proporcionar una semántica formal rigurosa sin dejar de ser accesible para cualquier programador Java. Existen diversas herramientas que utilizan las especificaciones de comportamiento de JML. Dado que las especificaciones pueden escribirse como anotaciones en archivos de programa Java o almacenarse en archivos de especificación independientes, los módulos Java con especificaciones JML pueden compilarse sin modificaciones con cualquier compilador Java.

Las especificaciones JML se agregan al código Java en forma de anotaciones en comentarios. Los comentarios Java se interpretan como anotaciones JML cuando comienzan con un signo @. Es decir, comentarios de la forma

//@ <Especificación JML>

o

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

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

requires

Define una condición previa para el método que se describe a continuación.

ensures

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

signals

Define una postcondición para cuando el método siguiente lanza una excepción determinada.

signals_only

Define qué excepciones pueden generarse cuando se cumple la condición previa dada.

assignable

Define a qué campos se les puede asignar un valor mediante el método que se describe a continuación.

pure

Declara que un método no tiene efectos secundarios (como assignable \nothingpero también puede lanzar excepciones). Además, se supone que un método puro siempre debe terminar normalmente o lanzar una excepción.

invariant

Define una propiedad invariante de la clase .

loop_invariant

Define un invariante de bucle para un bucle.

also

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

assert

Define una aserción JML .

spec_public

Declara una variable protegida o privada como pública a efectos de especificación.

JML básico también proporciona las siguientes expresiones

\result

Un identificador para el valor de retorno del método que se describe a continuación.

\old(<expression>)

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

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

El cuantificador universal .

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

El cuantificador existencial .

a ==> b

aimplicab

a <== b

aestá implícito porb

a <==> b

asi y solo sib

así como la sintaxis estándar de Java para los operadores lógicos AND, OR y NOT. Las anotaciones JML también tienen acceso a objetos Java, métodos de objetos y operadores que se encuentran dentro del ámbito del método anotado y que tienen la visibilidad adecuada. Estos se combinan para proporcionar especificaciones formales de las propiedades de las clases, los campos y los métodos. Por ejemplo, un ejemplo anotado de una clase bancaria simple podría verse 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; //@ ensure balance == 0; public BankingExample () { this . balance = 0 ; } //@ requires 0 < amount && amount + balance < MAX_BALANCE; //@ assignable balance; //@ ensure balance == \old(balance) + amount; public void credit ( final int amount ) { this . balance += amount ; } //@ requires 0 < amount && amount <= balance; //@ assignable balance; //@ ensure balance == \old(balance) - amount; public void debit ( final int amount ) { this . balance -= amount ; } //@ ensure isLocked == true; public void lockAccount () { this.isLocked = true ; } //@ requiere !isLocked; // @ asegura \result == balance; // @ también //@ requiere isLocked; //@ señales_only BankingException; public / *@ puro @*/ int getBalance ( ) throws BankingException { if ( ! this.isLocked ) { return this.balance ; } else { throw new BankingException ( ) ; } } }

La documentación completa de la sintaxis JML está disponible en el Manual de Referencia de JML .

Diversas herramientas ofrecen funcionalidades basadas en anotaciones JML. Las herramientas JML de la Universidad Estatal de Iowa incluyen un compiladorjmlc de comprobación de aserciones que convierte las anotaciones JML en aserciones en tiempo de ejecución, un generador de documentación jmldocque produce documentación Javadoc complementada con información adicional de las anotaciones JML, y un generador de pruebas unitarias jmlunitque genera código de prueba JUnit a partir de las anotaciones JML.

Grupos independientes están trabajando en herramientas que utilizan anotaciones JML. Estas incluyen:

• ESC/Java2, un verificador estático extendido que utiliza anotaciones JML para realizar una verificación estática más rigurosa de lo que sería posible de otro modo.
• OpenJML se declara sucesor de ESC/Java2.
• Daikon, archivado el 11 de diciembre de 2005 en Wayback Machine , es un generador invariante dinámico.
• KeY , que proporciona un demostrador de teoremas de código abierto con una interfaz JML y un complemento para Eclipse ( JML Editing ) con soporte para el resaltado de sintaxis de JML.
• Krakatoa Archivado el 8 de mayo de 2009 en Wayback Machine , una herramienta de verificación estática basada en la plataforma de verificación Why y que utiliza el asistente de prueba Rocq .
• JMLEclipse es un complemento para el entorno de desarrollo integrado Eclipse que admite la sintaxis JML e incluye interfaces con diversas herramientas que utilizan anotaciones JML.
• Sireum/Kiasan , un analizador estático basado en la ejecución simbólica que admite JML como lenguaje de contratos.
• JMLUnit , una herramienta para generar archivos para ejecutar pruebas JUnit en archivos Java anotados con JML.
• TACO es una herramienta de análisis de programas de código abierto que comprueba estáticamente el cumplimiento de un programa Java con respecto a la especificación del lenguaje de modelado Java (JML).

• Gary T. Leavens y Yoonsik Cheon. Diseño por contrato con JML ; tutorial de borrador.
• Gary T. Leavens , Albert L. Baker y Clyde Ruby. JML: Una notación para el diseño detallado ; en Haim Kilov, Bernhard Rumpe e Ian Simmonds (editores), Behavioral Specifications of Businesses and Systems , Kluwer, 1999, capítulo 12, páginas 175-188.
• Gary T. Leavens , Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin y Daniel M. Zimmerman. Manual de referencia de JML (BORRADOR), septiembre de 2009. HTML
• Marieke Huisman , Wolfgang Ahrendt, Daniel Bruns y Martin Hentschel. Especificación formal con JML . 2014. descargar (CC-BY-NC-ND)

• Sitio web de JML