Viquipèdia

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[1] (heredant idees d'Eiffel i Larch)[2] per especificar les precondicions, postcondicions i invariants d'un mètode.

Infotaula de lloc webJava Modeling Language (JML)
URLhttp://jmlspecs.sourceforge.net
Tipusllenguatge d'especificació Modifica el valor a Wikidata
Comerç ?NO
LlicènciaGNU General Public License version 2.0 (GPLv2)

Motivació

modifica

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.[3]

Avantatges de l'ús del JML

modifica

Els dos principals beneficis d'utilitzar el JML[4] 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

modifica

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.[4] Per exemple, no permet verificar l'accés coordinat a variables compartides ni verificar l'absència de deadlocks.

Sintaxi

modifica

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

modifica

La sintaxi més bàsica de JML[5][6] 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

modifica

Les expressions més bàsiques[5][6] 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

modifica

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).[7]
  • 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.[8]
  • 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).[9]
  • 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.[10]
  • 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.[11]
  • Sireum/Kiasan
Analitzador estàtic basat en una execució simbòlica que suporta JML com a llenguatge de contracte.[12]
  • JMLUnit
Eina que genera arxius per executar test JUnit sobre arxius Java amb anotacions JML.[13]
  • TACO
Programa d'anàlisi de codi obert que estàticament comprova el compliment de les especificacions JML d'un programa Java.[14]

Referències

modifica
  1. ↑ T. Leavens, Gary «Design by Contract with JML». Design by Contract with JML, 28-09-2006.
  2. ↑ T. Leavens, Gary «JML: A Notation for Detailed Design». JML: A Notation for Detailed Design.
  3. ↑ T. Leavens, Gary «[http://lib.dr.iastate.edu/cgi/viewcontent.cgi?article=1259&context=cs_techreports A Runtime Assertion Checker for the Java Modeling Language (JML)]». A Runtime Assertion Checker for the Java Modeling Language (JML), 01-04-2002.
  4. ↑ 4,0 4,1 T. Leavens, Gary. «What is JML Good For?» (en anglès). [Consulta: 2 setembre 2015].
  5. ↑ 5,0 5,1 «Summary of JML Features» (en anglès). [Consulta: 2 novembre 2015].[Enllaç no actiu]
  6. ↑ 6,0 6,1 «JML reference manual» (en anglès). [Consulta: 2 novembre 2015].
  7. ↑ «[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.161.9760&rep=rep1&type=pdf Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2]» (  PDF) (en anglès).
  8. ↑ D. Ernst, Michael «The Daikon system for dynamic detection of likely invariants» (en anglès). The Daikon system for dynamic detection of likely invariants, 03-11-2005.
  9. ↑ Stump, Aaron «[https://web.archive.org/web/20160304043225/http://vstte.ethz.ch/Files/stump.pdf Programming with Proofs: Language-Based Approaches to Totally Correct Software]» (  PDF) (en anglès). Programming with Proofs: Language-Based Approaches to Totally Correct Software. Arxivat de l'original el 2016-03-04 [Consulta: 31 maig 2023].
  10. ↑ Marché, C. «[http://www.ensiie.fr/~urbain/textes/marche04jlap.pdf The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML]» (  PDF) (en anglès). The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML.
  11. ↑ «JML Eclipse Plugin» (en anglès). [Consulta: 2 novembre 2015].
  12. ↑ «About Sireum» (en anglès). [Consulta: 2 novembre 2015].
  13. ↑ Cheon, Yoonsik «[http://lib.dr.iastate.edu/cgi/viewcontent.cgi?article=1177&context=cs_techreports A Simple and Practical Approach to Unit Testing: The JML and JUnit Way]» (en anglès). A Simple and Practical Approach to Unit Testing: The JML and JUnit Way, 01-11-2001.
  14. ↑ «TACO: Translation of Annotated COde» (en anglès). Arxivat de l'original el 2011-07-06. [Consulta: 2 novembre 2015].

Manuals

modifica
Obtingut de «https://ca.wikipedia.org/w/index.php?title=JML&oldid=33553774»