stringtranslate.com

Lenguaje de modelado Java

El lenguaje de modelado Java ( JML ) es un lenguaje de especificación para programas Java , que utiliza condiciones previas , poscondiciones e invariantes de estilo Hoare , que sigue el paradigma de diseño por contrato . Las especificaciones se escriben como comentarios de anotaciones de Java en los archivos fuente, que por lo tanto se pueden compilar con cualquier compilador de Java .

Varias herramientas de verificación, como un verificador de afirmaciones en tiempo de ejecución y el Comprobador 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 ambigüedades 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 y al mismo tiempo 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 pueden escribirse como anotaciones en archivos de programa Java o almacenarse en archivos de especificaciones separados, los módulos Java con especificaciones JML se pueden compilar sin cambios con cualquier compilador Java.

Sintaxis

Las especificaciones JML se agregan al código Java en forma de anotaciones en comentarios. Los comentarios de 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 JML básica proporciona las siguientes palabras clave

requires
Define una condición previa en el método siguiente.
ensures
Define una poscondición en el método siguiente.
signals
Define una poscondición para cuando el método siguiente genera una excepción determinada.
signals_only
Define qué excepciones se pueden lanzar cuando se cumple la condición previa dada.
assignable
Define qué campos se pueden asignar mediante el método siguiente.
pure
Declara que un método está libre de efectos secundarios (como assignable \nothingpero también puede generar excepciones). Además, se supone que un método puro siempre termina normalmente o genera una excepción.
invariant
Define una propiedad invariante de la clase .
loop_invariant
Define una 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 pública una variable protegida o privada para fines de especificación.

JML básico también proporciona las siguientes expresiones

\result
Un identificador para el valor de retorno del método siguiente.
\old(<expression>)
Un modificador para referirse al valor de <expression>en el momento de ingresar a 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 enb
a <==> b
asi y solo sib

así como la sintaxis estándar de Java para lógica and, or, and not. Las anotaciones JML también tienen acceso a objetos Java, métodos de objetos y operadores 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 comentado de una clase bancaria simple puede verse así

ejemplo bancario de clase pública { public static final int MAX_BALANCE = 1000 ; privado /*@ spec_public @*/ int saldo ; privado /*@ spec_public @*/ booleano isLocked = false ; //@ saldo público invariante >= 0 && saldo <= MAX_BALANCE; //@ saldo asignable; //@ asegura el saldo == 0; ejemplo de banca pública () { this . saldo = 0 ; } //@ requiere 0 < monto && monto + saldo < MAX_BALANCE; //@ saldo asignable; //@ asegura el saldo == \old(saldo) + importe; crédito público nulo ( monto int final ) { this . saldo += importe ; } //@ requiere 0 < monto && monto <= saldo; //@ saldo asignable; //@ asegura el saldo == \old(saldo) - monto; débito público nulo ( monto int final ) { this . saldo -= monto ; } //@ asegura que está bloqueado == true; cuenta de bloqueo pública nula () { esto . está bloqueado = verdadero ; } //@ requiere !isLocked; //@ asegura \resultado == saldo; //@ también //@ requiere isLocked; //@ señales_solo BankingException; public /*@ pure @*/ int getBalance () lanza BankingException { if ( ! this . isLocked ) { return this . balance ; } else { lanzar nueva BankingException (); } } }

La documentación completa de la sintaxis 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 jmlc de verificación de aserciones que convierte anotaciones JML en aserciones en tiempo de ejecución, un generador de documentación jmldocque produce documentación Javadoc aumentada con información adicional de anotaciones JML y un generador de pruebas unitarias jmlunitque genera código de prueba JUnit a partir de anotaciones JML.

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

Referencias

enlaces externos