El Lenguaje de Modelado de Java ( JML ) es un lenguaje de especificación de Java programas, utilizando Hoare estilo pre y post-condiciones y invariantes , que sigue el diseño por contrato paradigma. Las especificaciones se escriben como comentarios de anotaciones de Java en los archivos de origen, que por lo tanto se pueden compilar con cualquier compilador de Java .
Varias herramientas de verificación, como un verificador de aserciones en tiempo de ejecución y el verificador estático extendido ( ESC / Java ) ayudan al desarrollo.
Descripción general
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 la ambigüedad con respecto a las intenciones de los diseñadores del módulo. JML hereda ideas de Eiffel , Larch y Refinement Calculus , con el objetivo de proporcionar una semántica formal rigurosa sin dejar de ser accesible para cualquier programador de Java. Hay varias herramientas disponibles que hacen uso de las especificaciones de comportamiento de JML. Debido a que las especificaciones se pueden escribir como anotaciones en archivos de programa de Java, o se pueden almacenar en archivos de especificación separados, los módulos de Java con especificaciones JML se pueden compilar sin cambios con cualquier compilador de Java.
Sintaxis
Las especificaciones JML se agregan al código Java en forma de anotaciones en los comentarios. Los comentarios de Java se interpretan como anotaciones JML cuando comienzan con un signo @. Es decir, comentarios del formulario
// @ón>
o
/ * @@ * / ón>
La sintaxis básica de JML proporciona las siguientes palabras clave
requires
- Define una condición previa en el método que sigue.
ensures
- Define una condición posterior en el método que sigue.
signals
- Define una condición posterior para cuando una excepción dada es lanzada por el método que sigue.
signals_only
- Define qué excepciones se pueden lanzar cuando se cumple la condición previa dada.
assignable
- Define qué campos pueden asignarse mediante el método siguiente.
pure
- Declara que un método no tiene efectos secundarios (como,
assignable \nothing
pero también puede generar excepciones). Además, se supone que un método puro siempre termina normalmente o lanza una excepción. invariant
- Define una propiedad invariante de la clase .
loop_invariant
- Define un ciclo invariante para un ciclo.
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 pública una variable protegida o privada para fines de especificación.
Basic JML también proporciona las siguientes expresiones
\result
- Un identificador para el valor de retorno del método que sigue.
\old(
) - Un modificador para hacer referencia al valor de
en el momento de la entrada en un método. (\forall
; ; ) - El cuantificador universal .
(\exists
; ; ) - El cuantificador existencial .
a ==> b
a
implicab
a <== b
a
está implícito enb
a <==> b
a
si y solo sib
así como la sintaxis estándar de Java para lógica and, or y not. Las anotaciones JML también tienen acceso a los objetos, métodos de objeto y operadores de Java que están dentro del alcance del método que se está anotando y que tienen la visibilidad adecuada. Estos se combinan para proporcionar especificaciones formales de las propiedades de clases, campos y métodos. Por ejemplo, un ejemplo anotado de una clase bancaria simple puede verse como
public class BankingExample { public static final int MAX_BALANCE = 1000 ; privado / * @ spec_public @ * / int balance ; privado / * @ spec_public @ * / boolean isLocked = false ; // @ balance invariante público> = 0 && balance <= MAX_BALANCE; // @ saldo asignable; // @ asegura el equilibrio == 0; public BankingExample () { this . saldo = 0 ; } // @ requiere 0 // @ saldo asignable; // @ asegura el saldo == \ antiguo (saldo) + monto; crédito público nulo ( monto final int ) { this . saldo + = monto ; } // @ requiere 0 // @ saldo asignable; // @ asegura el saldo == \ antiguo (saldo) - monto; débito público nulo ( monto final int ) { this . saldo - = monto ; } // @ asegura que está bloqueado == verdadero; public void lockAccount () { esto . isLocked = true ; } // @ requiere! isLocked; // @ asegura \ resultado == equilibrio; // @ también // @ requiere isLocked; // @ señales_only BankingException; public / * @ pure @ * / int getBalance () lanza BankingException { if ( ! this . isLocked ) { return this . equilibrar ; } else { lanzar nueva BankingException (); } } }
La documentación completa de la sintaxis de JML está disponible en el Manual de referencia de JML .
Soporte de herramientas
Una variedad de herramientas proporcionan funcionalidad basada en anotaciones JML. Las herramientas JML del estado de Iowa proporcionan un compilador de verificación de afirmaciones jmlc
que convierte las anotaciones JML en afirmaciones en tiempo de ejecución, un generador de documentación jmldoc
que produce documentación Javadoc aumentada con información adicional de anotaciones JML y un generador de pruebas unitarias jmlunit
que genera código de prueba JUnit a partir de anotaciones JML.
Grupos independientes están trabajando en herramientas que utilizan anotaciones JML. Éstas incluyen:
- ESC / Java2 [1] , un verificador estático extendido que usa anotaciones JML para realizar una verificación estática más rigurosa de lo que sería posible de otra manera.
- OpenJML se declara el sucesor de ESC / Java2.
- Daikon , un generador invariante dinámico.
- KeY , que proporciona un probador de teoremas de código abierto con un front-end JML y un complemento Eclipse ( edición JML ) con soporte para resaltado de sintaxis de JML.
- Krakatoa , una herramienta de verificación estática basada en la plataforma de verificación Why y utilizando el asistente de pruebas Coq .
- JMLEclipse , un complemento para el entorno de desarrollo integrado de Eclipse con soporte para sintaxis JML e interfaces para varias herramientas que hacen uso de anotaciones JML.
- Sireum / Kiasan , un analizador estático basado en ejecución simbólica que admite JML como lenguaje de contrato.
- JMLUnit , una herramienta para generar archivos para ejecutar pruebas JUnit en archivos Java con anotaciones JML.
- TACO , una herramienta de análisis de programas de código abierto que verifica estáticamente la conformidad de un programa Java con su especificación Java Modeling Language.
- Verificador de VerCors
Referencias
- Gary T. Leavens y Yoonsik Cheon. Diseño por contrato con JML ; Proyecto de tutorial.
- 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), Especificaciones de comportamiento de empresas y sistemas , 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)
enlaces externos
- Sitio web de JML