AccueilđŸ‡«đŸ‡·Chercher

Java Modeling Language

Le Java Modeling Language (JML) est un langage de spécification pour Java, il est basé sur le paradigme de la programmation par contrat. Il utilise la logique de Hoare, les pré et postconditions ainsi que les invariants. Les spécifications sont ajoutées dans les commentaires du code en Java, elles sont ensuite compilées par le compilateur Java.

Il existe divers outils de vérification pour JML, tels qu'un exécutable de vérification d'assertions et que l'Extended Static Checker (ESC/Java).

Présentation

JML est un langage de spĂ©cification pour les rĂ©alisations en Java. Il fournit une sĂ©mantique pour dĂ©crire formellement le comportement des programmes Java. Son but est d'enlever les potentielles ambiguĂŻtĂ©s du programme par rapport aux intentions du concepteur. JML peut ĂȘtre comparĂ© Ă  la programmation par contrat de Eiffel et de la famille Larch. Son but est de fournir une sĂ©mantique de vĂ©rification formelle rigoureuse restant accessible Ă  tout programmeur Java. Les spĂ©cifications peuvent ĂȘtre Ă©crites directement dans les commentaires du code Java, ou enregistrĂ©es dans un fichier de spĂ©cification sĂ©parĂ©. Divers outils peuvent tirer parti de ces informations supplĂ©mentaires fournies par les spĂ©cifications JML. De plus, comme les annotations JML prennent la forme de commentaires, les programmes comportant de telles spĂ©cifications peuvent ĂȘtre compilĂ©s directement par n'importe quel compilateur Java.

Syntaxe

Les spécifications JML sont ajoutées au code Java sous forme d'annotations dans les commentaires. Ces commentaires Java sont interprétés comme annotations JML lorsqu'ils commencent par un @. Exemple de commentaires JML :

//@ <Spécifications JML>

ou

/*@ <Spécification JML> @*/

La syntaxe de base de JML est basée sur les mots-clés suivants :

requires
Définit une précondition pour la méthode qui suit.
ensures
Définit une postcondition pour la méthode qui suit.
signals
DĂ©finit une condition dĂ©terminant quand une exception donnĂ©e peut ĂȘtre lancĂ©e par la mĂ©thode qui suit.
assignable
Définit quels attributs sont assignables par la méthode qui suit.
pure
Déclare une méthode pure, sans effet de bord ne modifiant rien (comme pour assignable \nothing mais peut lancer des exceptions).
invariant
Définit une propriété invariante de la classe.
also
Permet la déclaration de sur spécifications pour rajouter aux spécifications héritées de la superclasse.
assert
DĂ©finit une assertion JML.

Le JML fournit aussi de base les expressions suivantes :

\result
Un identifiant pour la valeur de retour de la méthode qui suit.
\old(<name>)
Un modificateur pour se reporter à la valeur de la variable <name> au moment de l'appel de la méthode.
\forall
Le quantificateur universel, pour tout.
\exists
Le quantificateur existentiel, il existe.
a ⇒ b
La relation logique a implique b
a ⇔ b
La relation logique a Ă©quivaut Ă  b

ainsi que les éléments logiques standards et, ou, et non de la syntaxe Java. Les annotations JML ont aussi accÚs aux objets Java, aux méthodes et opérateurs accessibles par la méthode annotée. Tous ces éléments sont combinés pour fournir une spécification formelle des propriétés des classes, attributs et méthodes. Par exemple, le code suivant correspond est un exemple simple d'une classe de compte bancaire annotée de spécifications JML :

public class CompteBancaireExemple {
    public static final int MAX_SOLDE = 1000; 
    private int solde;
    private boolean isLocked = false; 
    //@ invariant solde >= 0 && solde ⇐ MAX_SOLDE;
    //@ assignable solde;
    //@ ensures solde == 0;
    public CompteBancaireExemple() { ... }
    //@ requires montant > 0;
    //@ ensures solde == \old(solde) + montant;
    //@ assignable solde;
    public void crediter(int montant) { ... }
    //@ requires montant > 0;
    //@ ensures solde == \old(solde) - montant;
    //@ assignable solde
    public void debiter(int montant) { ... }
    //@ ensures isLocked == true;
    public void lockCompte() { ... }
    //@ signals (CompteBancaireException e) isLocked;
    public /*@ pure @*/ int getSolde() throws CompteBancaireException { ... }
}

Outils

Il existe des outils variés offrant des fonctionnalités basée sur les annotations JML. L'outil Iowa State JML permet de convertir les annotations JML en exécutable d'assertions via un compilateur de vérification d'assertion jmlc, de générer une Javadoc améliorée incluant des informations tirées des spécifications JML, et de générer des tests unitaires pour JUnit via le générateur jmlunit.

En plus de cet outil, des groupes indĂ©pendants travaillent sur des outils utilisant JML. Parmi ceux-ci : « ESC/Java2 »(Archive.org ‱ Wikiwix ‱ Archive.is ‱ Google ‱ Que faire ?), Extended Static Checker qui utilise les annotations JML pour effectuer une vĂ©rification statique plus rigoureuse que celle autrement possible; Daikon, un gĂ©nĂ©rateur d'invariant dynamique; KeY, un vĂ©rificateur de thĂ©orĂšmes; Krakatoa, un vĂ©rificateur de thĂ©orĂšmes basĂ© sur l'assistant de preuve Coq; et JMLeclipse, un plugin pour Eclipse l'environnement de dĂ©veloppement intĂ©grĂ©.

Références

  • Gary T. Leavens, Yoonsik Cheon. Design by Contract with JML. Draft tutorial.
  • Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, chapter 12, pages 175-188. Kluwer, 1999.

Liens externes

Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplĂ©mentaires peuvent s’appliquer aux fichiers multimĂ©dias.