El Java Modeling Language ( JML ) es una especificación de lenguaje para Java , se basa en el paradigma de la programación por contrato . Utiliza la lógica de Hoare , las condiciones previas y posteriores, así como las invariantes . Las especificaciones se agregan en los comentarios del código en Java, luego son compiladas por el compilador de Java.
Hay varias herramientas de verificación para JML, como un ejecutable de verificación de aserción y el Verificador estático extendido (ESC / Java).
JML es un lenguaje de especificación para implementaciones en Java . Proporciona semántica para describir formalmente el comportamiento de los programas Java. Su objetivo es eliminar las posibles ambigüedades del programa en relación con las intenciones del diseñador. JML se puede comparar con la programación por contrato de Eiffel y la familia Larch. Su objetivo es proporcionar una semántica de verificación formal rigurosa que permanezca accesible para cualquier programador de Java. Las especificaciones se pueden escribir directamente en el código Java de comentarios o se pueden almacenar en un archivo de especificación separado. Varias herramientas pueden aprovechar esta información adicional proporcionada por las especificaciones JML. Además, dado que las anotaciones JML toman la forma de comentarios, cualquier compilador de Java puede compilar directamente programas con tales especificaciones.
Las especificaciones JML se agregan al código Java como anotaciones en los comentarios. Estos comentarios de Java se interpretan como anotaciones JML cuando comienzan con @. Ejemplo de comentarios JML:
//@ <Spécifications JML>o
/*@ <Spécification JML> @*/La sintaxis básica de JML se basa en las siguientes palabras clave:
requires Define una condición previa para el siguiente método . ensures Define una condición posterior para el siguiente método . signals Define una condición que determina cuándo se puede generar una excepción determinada mediante el siguiente método. assignable Define qué atributos se pueden asignar mediante el siguiente método. pure Declare un método puro, sin efectos secundarios que no cambien nada (como, assignable \nothingpero pueden generar excepciones). invariant Define una propiedad invariante de la clase . also Permite que la declaración de sobreespecificaciones se agregue a las especificaciones heredadas de la superclase. assert Define una aserción JML.El JML también proporciona las siguientes expresiones básicas:
\result Un identificador para el valor de retorno del siguiente método. \old(<name>) Un modificador para hacer referencia al valor de la variable <name>cuando se llama al método. \forall El cuantificador universal, para todo. \exists El cuantificador existencial, lo hay. a ⇒ b La relación lógica aimplicab a ⇔ b La relación lógica es aequivalente abasí como elementos lógicos estándar y, o, y no sintaxis Java. Las anotaciones JML también tienen acceso a los objetos, métodos y operadores de Java accesibles mediante el método anotado. Todos estos elementos se combinan para proporcionar una especificación formal de las propiedades de clases, atributos y métodos. Por ejemplo, el siguiente código corresponde a un ejemplo simple de una clase de cuenta bancaria anotada de especificación JML:
public class CompteBancaireExemple { public static final int MAX_SOLDE = 1000; private int solde; private boolean isLocked = false; //@ invariant solde >= 0 && solde ⇐ MAX_SOLDE; //@ assignable solde; //@ ensures solde == 0; public CompteBancaireExemple() { ... } //@ requires montant > 0; //@ ensures solde == \old(solde) + montant; //@ assignable solde; public void crediter(int montant) { ... } //@ requires montant > 0; //@ ensures solde == \old(solde) - montant; //@ assignable solde public void debiter(int montant) { ... } //@ ensures isLocked == true; public void lockCompte() { ... } //@ signals (CompteBancaireException e) isLocked; public /*@ pure @*/ int getSolde() throws CompteBancaireException { ... } }Hay varias herramientas que ofrecen funciones basadas en anotaciones JML. La herramienta Iowa State JML puede convertir anotaciones JML en ejecutables de aserción a través de un compilador de verificación de aserciones jmlc, generar un Javadoc mejorado que incluye información de las especificaciones de JML y generar pruebas unitarias para JUnit a través del generador jmlunit.
Además de esta herramienta, grupos independientes están trabajando en herramientas que utilizan JML. Entre estos: " ESC / Java2 " ( Archivo • Wikiwix • Archive.is • Google • ¿Qué hacer? ) , Comprobador estático extendido que utiliza anotaciones JML para realizar una comprobación estática más rigurosa de lo que sería posible; Daikon , un generador invariante dinámico; KeY , un verificador de teoremas; Krakatoa , un verificador de teoremas basado en el asistente de pruebas de Coq ; y JMLeclipse , un complemento para el entorno de desarrollo integrado de Eclipse .