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.
Motivació La depuració (en anglès debugging) es fa difícil per la necessitat de descriure amb precisió el que se suposa que cada part del programari ha de fer i escriure el codi per protegir els mòduls contra els errors dels altres mòduls; si no es fa això, és difícil donar la culpa a una part petita del programa quan les coses no funcionen correctament. De la mateixa manera, els testos unitaris també necessiten descripcions precises del comportament i es fa difícil per la necessitat d'escriure testos oracles (mecanisme per determinar si el programa ha passat o no una prova). No obstant, la depuració i el testeig requereixen una fracció significativa del cost de desenvolupament de programari i els esforços de manteniment. Una depuració i proves inadequades també contribueixen als problemes de qualitat. Descrivim un runtime assertion checker (comprovador d'afirmacions en temps d'execució) pel Java Modeling Language (JML) que ajuda a donar la culpa durant la depuració i la generació automàtica dels testos oracles. Representa un avanç significatiu sobre l'estat actual de la tècnica, perquè pot fer front a especificacions molt abstractes que amaguen les dades de representació i altres característiques com ara quantificadors i l'herència de les especificacions. No obstant, les especificacions JML tenen una sintaxi que és fàcil d'entendre pels programadors. Per tant, JML's runtime assertion checker té el potencial per disminuir el cost de depuració i testeig.
Avantatges de l'ús del JML Els dos principals beneficis d'utilitzar el JML són: La precisió a l'hora d'especificar el mòduls i documentar el codi de programes en Java, evitant ambigüetats. 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 se 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.
Sintaxi Les assercions JML s'escriuen en forma de comentari als arxius .java, i són interpretades com a tals quan comencen amb el símbol @. Els comentaris tenen una d'aquestes dues formes://@ <Especificació JML> /*@ <Especificació JML> */
Paraules clau La sintaxi més bàsica de JML comprèn les paraules clau següents: requires Defineix la precondició pel mètode que precedeix. ensures Defineix una postcondició pel mètode que precedeix. signals Indica en quins casos es llança una excepció en el mètode que precedeix. signals_only Indica quines excepcions es poden llançar en cas de violar la precondició en el mètode que precedeix. assignable Defineix quins arguments poden ser modificats pel mètode que precedeix. pure Indica que el mètode no té efectes laterals. És sinònim deassignable \nothing. invariant Defineix la invariant d'una classe. loop_invariant Defineix la invariant d'un bucle. also Permet combinar casos d'especificació. També pot indicar que un mètode hereda les especificacions del seu supertipus. assert Defineix una asserció JML. spec_public Declara una variable privada o protegida com a pública, només per a fins d'especificació.
Expressions Les expressions més bàsiques del JML són: \result Identifica el valor de retorn d'un mètode. \old(<expressió>) Permet referir-se al valor de <expressió> abans d'entrar al mètode. (\forall <declaració>; <rang-expressió>; <expressió>) El quantificador universal. Exemple d'ús: (\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j]) (\exists <declaració>; <rang-expressió>; <expressió>) El quantificador existencial. Exemple d'ús: (\exists int i,j; 0 <= i && i < j && j < 10; a[i] < a[j]) a ==> b a implica b a <== b a és implicat per b a <==> b a si i només si (sii) b
Eines de suport Existeixen una sèrie d'eines que proveeixen unes funcionalitats basades en anotacions JML. Les eines del grup JML de la Universitat de Florida Central (formalment lowa State JML) proporcionen un compilador jmlc que verifica les assercions i les converteix en anotacions JML en temps d'execució, un generador de documentació jmldoc que genera documentació Javadoc ampliada amb informació addicional de les anotacions JML i un generador de tests unitaris jmlunit que genera codi de prova JUnit a partir de les anotacions JML.
També hi ha grups independents que treballen en eines que facin ús de les anotacions JML, entre elles: 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 (per exemple, NullPointerException). Daikon Daikon és una implantació de detecció dinàmica de possibles invariants. Una invariant és una propietat que s'ha de complir en un determinat punt o punts d'un programa; s'utilitza sovint en declaracions assert, documentació i especificacions formals. KeY L'eina KeY s'utilitza en la verificació formal de programes Java. Accepta les especificacions escrites en JML d'arxius fonts Java. Aquests es transformen en teoremes de lògica dinàmica i després es comparen contra la semàntica del programa que també són definides en termes de lògica dinàmica. KeY és una eina molt potent, ja que suporta tant interactius (és a dir, a mà) com proves de correctessa totalment automatitzades. Les proves que han fallat poden ser utilitzades per una depuració més eficient o per proves basades en la verificació (verification-based testing). Krakatoa Krakatoa és una eina de verificació estàtica del programes Java basat en la plataforma de verificació Why utilitzant l'assistent d'evidència Coq. Tracta amb les anotacions JML dels programes Java. JMLeclipse Connector (en anglès plugin) per a l'IDE Eclipse amb suport de sitaxi JML i interfícies a diferents eines que utilitzen anotacions JML. Sireum/Kiasan Analitzador estàtic basat en una execució simbòlica que suporta JML com a llenguatge de contracte. JMLUnit Eina que genera arxius per executar test JUnit sobre arxius Java amb anotacions JML. TACO Programa d'anàlisi de codi obert que estàticament comprova el compliment de les especificacions JML d'un programa Java.
Referències
Manuals Introducció al JML Tutorial extens de JML Més exemples
Categoria:Java