Editando Java Modeling Language (sección)

== Herramientas de soporte ==
Una serie de herramientas proveen funcionalidad basada en las anotaciones JML. Las herramientas de la Iowa State JML otorgan un compilador que verifica las aserciones <code>jmlc</code> que convierte las anotaciones JML en aserciones de [[tiempo de ejecución]], un generador de documentos <code>jmldoc</code> que produce documentación [[Javadoc]] ampliada con información extra de las anotaciones JML y un generador de tests de módulos <code>jmlunit</code> que genera un marco para tests [[JUnit]] a partir de las anotaciones JML.

También hay grupos independientes que trabajan en herramientas que hacen uso de las anotaciones JML, entre ellas:
* [[ESC/Java2]] [https://web.archive.org/web/20110514011545/http://secure.ucd.ie/products/opensource/ESCJava2/], un verificador estático extendido que utiliza anotaciones JML;
* [http://pag.csail.mit.edu/daikon/ Daikon], un generador invariante dinámico;
* [[KeY]], que provee un comprobador de teorema con una fachada JML;
* [http://krakatoa.lri.fr/ Krakatoa], una herramienta de verificación estática basada en la plataforma de verificación [http://why.lri.fr/ Why] y utilizando el asistente de evidencia [[Coq]];
* [http://jmleclipse.projects.cis.ksu.edu/ JMLeclipse], un plugin para el [[Integrated Development Environment|IDE]] [[Eclipse (software)|Eclipse]] con soporte de sintaxis JML e interfaces a varias herramientas que utilizan anotaciones JML.
* [http://www.sireum.org/?q=node/21/ Sireum/Kiasan], un analizador estático basado en una ejecución simbólica que soporta JML como lenguaje de contrato.
* [https://www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlunit.html JMLUnit], una herramienta que genera archivos para ejecutar tests JUnit sobre archivos Java con anotación JML.
* [https://web.archive.org/web/20110706084805/http://www.dc.uba.ar/inv/grupos/rfm_folder/TACO TACO], programa de análisis de código abierto que estáticamente comprueba el cumplimiento de un programa de Java frente a su especificación en JML.