Usuari:Ramon Viñas Torné/proves/JML

El Llenguatge de Modelatge per Java (JML, Java Modeling Language) és un llenguatge d’especificació que s’utilitza per documentar formalment el comportament dels mòduls de programes en Java. Segueix el paradigma del disseny per contracte (heredant idees d’Eiffel i Larch) per especificar les precondicions, postcondicions i invariants d’un mètode.

Avantatges de l'ús del JML

Els dos principals beneficis d’utilitzar el JML són:

1. La precisió a l’hora d’especificar el mòduls i documentar el codi de programes en Java, evitant ambigüetats.
2. La possibilitat d’utilitzar eines de suport que, en temps d’execució, converteixen les anotacions JML en assercions i les verifiquen, entre d’altres. Permet raonar sobre la correctesa d’un codi i fer-ne una verificació formal del seu funcionament.

Limitacions del JML

La versió actual de JML es centra en el comportament seqüencial dels codi Java i no té suport pels aspectes concurrents del codi Java. Per exemple, no permet verificar l’accés coordinat a variables compartides ni verificar l’absència de deadlocks.

Eines de suport

ESC/Java

És una eina per programes en Java que permet trobar errors d’execució en temps de compilació. No garanteix trobar-los tots, però permet detectar ràpidament bugs importants. A més, és una bona eina a l’hora de notar l’absència d’excepcions Runtime (ex: NullPointerException, ArrayIndexOutOfBounds, ClassCastException,…).

L’eina ESC/Java força l’especificació de totes propietats del codi (invariants, precondicions i postcondicions), amb les quals l’eina es basarà per fer la verificació. Amb aquestes propietats documentades, entendre el codi és més fàcil.