Contrariamente a los contratos de código en C#, en el código JML los contratos son solo texto que se utiliza en forma de comentarios en el encabezado de un método. ¿No sería mejor tenerlos expuestos como Anotaciones, entonces? De esta forma, incluso cuando se compila, la información persistiría en los metadatos de .class, contrariamente a los comentarios, que se borrarían.¿Por qué no se implementa JML como anotaciones en Java?
¿Echo de menos algo?
+1 - Las fechas de copyright en el informe técnico "borrador de especificación" son 1998-2006. –