Worldlex Wiki Divers outils de vérification, tels qu'un vérificateur d'assertions d'exécution et le vérificateur statique étendu ( ESC/Java ), facilitent le développement.
une sémantique permettant de décrire formellement le comportement d'un module Java, évitant ainsi toute ambiguïté quant aux intentions des concepteurs. JML s'inspire d' Eiffel , de Larch et du calcul de raffinement , avec pour objectif de fournir une sémantique formelle rigoureuse tout en restant accessible à tout programmeur Java. Divers outils exploitent les spécifications comportementales de JML. Ces spécifications pouvant être écrites sous forme d'annotations dans les fichiers de programme Java ou stockées dans des fichiers de spécification séparés, les modules Java dotés de spécifications JML peuvent être compilés sans modification avec n'importe quel compilateur Java.Syntaxe
Les spécifications JML sont ajoutées au code Java sous forme d'annotations dans les commentaires. Les commentaires Java sont interprétés comme des annotations JML lorsqu'ils commencent par le symbole @. Autrement dit, les commentaires de la forme suivante :
ensuressignalssignals_onlyassignablepureassignable othing, mais pouvant également lever des exceptions). De plus, une méthode pure est censée toujours se terminer normalement ou lever une exception.invariantloop_invariantalsoassertspec_publicJML de base fournit également les expressions suivantes
esult- Un identifiant pour la valeur de retour de la méthode qui suit.
\old(<expression>)- Un modificateur permettant de faire référence à la valeur de
<expression>au moment de l'entrée dans une méthode. (\forall <decl>; <range-exp>; <body-exp>)- Le quantificateur universel .
(\exists <decl>; <range-exp>; <body-exp>)- Le quantificateur existentiel .
a ==> baimpliqueba <== baest sous-entendu parba <==> basi et seulement sib
ainsi que la syntaxe Java standard pour les opérateurs logiques ET, OU et NON. Les annotations JML permettent également d'accéder aux objets, méthodes et opérateurs Java qui se trouvent dans la portée de la méthode annotée et qui disposent de la visibilité appropriée. Ces éléments sont combinés pour fournir des spécifications formelles des propriétés des classes, des champs et des méthodes. Par exemple, une classe bancaire simple annotée pourrait ressembler à ceci :
public class BankingExample { public static final int MAX_BALANCE = 1000 ; private /*@ spec_public @*/ int balance ; private /*@ spec_public @*/ boolean isLocked = false ; //@ public invariant balance >= 0 && balance <= MAX_BALANCE; //@ assignable balance; //@ ensures balance == 0; public BankingExample () { this . balance = 0 ; } //@ requires 0 < amount && amount + balance < MAX_BALANCE; //@ assignable balance; //@ ensures balance == \old(balance) + amount; public void credit ( final int amount ) { this . balance += amount ; } //@ requires 0 < amount && amount <= balance; //@ assignable balance; //@ ensures balance == \old(balance) - amount; public void debit ( final int amount ) { this . balance -= amount ; } //@ ensures isLocked == true; public void lockAccount () { this.isLocked = true ; } //@ requires !isLocked; //@ ensures esult == balance; // @ also // @ requires isLocked; //@ signals_only BankingException; public /*@ pure @*/ int getBalance ( ) throws BankingException { if ( ! this.isLocked ) { return this.balance ; } else { throw new BankingException ( ) ; } } }
La documentation complète de la syntaxe JML est disponible dans le manuel de référence JML .
Assistance technique
Divers outils offrent des fonctionnalités basées sur les annotations JML. Les outils JML de l'Iowa State University proposent un compilateurjmlc de vérification d'assertions qui convertit les annotations JML en assertions d'exécution, un générateur de documentation jmldocqui produit une documentation Javadoc enrichie d'informations supplémentaires issues des annotations JML, et un générateur de tests unitaires jmlunitqui génère du code de test JUnit à partir des annotations JML.
Des groupes indépendants travaillent sur des outils qui utilisent les annotations JML. Parmi ceux-ci :
- ESC/Java2, un vérificateur statique étendu qui utilise les annotations JML pour effectuer des vérifications statiques plus rigoureuses que ce qui est possible autrement.
- OpenJML se déclare successeur d'ESC/Java2.
- Daikon le 11 décembre 2005 sur la Wayback Machine , un générateur d'invariants dynamiques.
- KeY , qui fournit un démonstrateur de théorèmes open source avec une interface JML et un plug-in Eclipse ( JML Editing ) prenant en charge la coloration syntaxique du JML.
- Krakatoa le 08/05/2009 sur la Wayback Machine , est un outil de vérification statique basé sur la plateforme de vérification Why et utilisant l' assistant de preuve Rocq .
- JMLEclipse est un plugin pour l'environnement de développement intégré Eclipse prenant en charge la syntaxe JML et offrant des interfaces avec divers outils utilisant les annotations JML.
- Sireum/Kiasan , un analyseur statique basé sur l'exécution symbolique qui prend en charge JML comme langage de contrat.
- JMLUnit , un outil permettant de générer des fichiers pour exécuter des tests JUnit sur des fichiers Java annotés JML.
- TACO , un outil d'analyse de programmes open source qui vérifie statiquement la conformité d'un programme Java à sa spécification Java Modeling Language.
- Gary T. Leavens et Yoonsik Cheon. Conception par contrat avec JML ; Tutoriel préliminaire.
- Gary T. Leavens , Albert L. Baker et Clyde Ruby. JML : une notation pour la conception détaillée ; dans Haim Kilov, Bernhard Rumpe et Ian Simmonds (éditeurs), Spécifications comportementales des entreprises et des systèmes , Kluwer, 1999, chapitre 12, pages 175-188.
- Gary T. Leavens , Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin et Daniel M. Zimmerman. Manuel de référence JML (ÉBAUCHE), septembre 2009. HTML
- Marieke Huisman , Wolfgang Ahrendt, Daniel Bruns et Martin Hentschel. Spécification formelle avec JML . 2014. télécharger (CC-BY-NC-ND)