JML (Java Modeling Language)

JML (Java Modeling Language)

JML es un lenguaje de modelado que permite realizar el Diseño por Contrato (Desing by Contract DBC) en java,  DBC es una metodología de desarrollo, que consiste en que  las clases y sus clientes tienen un contrato entre sí, los clientes antes de invocar un método de la clase deben garantizar ciertas condiciones de los datos de entrada y la clase debe garantizar cierto comportamiento y ciertas condiciones después de la ejecución de cada uno de sus  métodos, si alguno de los actores incumple con estas condiciones se produce un error o fallo del programa. Estas condiciones que el cliente y la clase deben cumplir se expresan en forma de Pre-Condiciones y Post-Condiciones en un lenguaje formal, por medio de anotaciones en el código java.

En resúmen, en la programación orientada por contrato, el cliente asegura la precondición y asume que la postcondición se cumple, y el método asume como cierta la precondición y asegura la postcondición.

Las especificaciones de JML, se escriben como comentarios especiales en java que empiezan con /@* y se cierran @*/, JML utiliza la cláusula requires para especificar las pre -condiciones u obligaciones del cliente y la cláusura ensures para las post-condiciones u obligaciones de la clase. JML debe validar que la pre-condición se cumpla  antes de llamar el método y garantizar qe la post-condición sea verdadera después de la ejecución del método. JML también permite expresar aserciones assert e invariantes invariant.

La sintaxis de JML es similar a la de java, y provee varios operadores que pueden ser utilizados: \result, \old, \sum, \forall 

JML también puede ser usado como documentación, puesto que la especificación escrita en JML, proporciona la claridad necesaria de lo que el método debe recibir y los resultados que debe arrojar, existe una herramienta denominada JML Doc, que genera la documentación con base en las anotaciones JML, una ventaja adicional de esta documentación además de ser breve y consistente, es que no tiene varias interpretaciones, puesto que la especificación formal no da lugar a ambigüedades.

JML evita la realización de validaciones innecesarias de los datos de entrada dentro de los métodos, puesto que la validez de los mismos están dados por las precondiciones establecidas, así mismo, facilita determinar si las fallas que se presentan corresponden a errores de implementación de los métodos o a fallas en los datos de entrada.

Conclusiones acerca de JML.

Aunque el alcance que se pretende obtener con la especificación del lenguaje JML, es muy amplio e interesante, las herramientas que lo implementan, aún son inmaduras y presentan muchos errores e inconsistencias, en el caso mío probé el plugin JML para eclipse y el verificador Z3_N3.

La verificación estática, puede detectar algunos posibles problemas en la codificación de los métodos, pero sigue siendo en tiempo de ejecución que se pueden detectar los errores de incumplimiento en los contratos de pre y/o post condiciones, lo cual no proporciona un valor agregado, puesto que sin el uso de JML, de todos modos el software lanzaría una excepción, lo que logramos en JML es cambiar la excepción que lanzaría el programa por una asociada a JML.

El ejercicio de escribir las condiciones del contrato, hace que el programador sea más conciente del comportamiento que debe tener la clase que va a desarrollar.

El uso de JML, invita a usar una metodología TDD, porque es muy importante escribir las pruebas o reglas del contrato de servicio de la clase en términos de pre y postcondiciones, antes de escribir el código que implementa la funcionalidad.