Java Modeling Language
Las especificaciones se escriben como comentarios de anotación Java en el código fuente, que por consiguiente puede compilarse con cualquier compilador de Java.Para facilitar el desarrollo existen varias herramientas de verificación, tales como programas que chequean el código antes de su ejecución (ej.Las especificaciones JML se agregan al código Java como anotaciones en los comentarios.Los comentarios Java se interpretan entonces como anotaciones JML cuando comienzan con el signo «@».Una serie de herramientas proveen funcionalidad basada en las anotaciones JML.