# 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 des commentaires spéciaux du code Java.
Il existe divers outils de vérification pour JML, tels que la vérification d'assertions à l'exécution (RAC) et la vérification statique (ESC/Java, OpenJML).

## Présentation

JML est un langage de spécification pour les programmes 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 est inspiré par 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 :
ou
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 :

## 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 assertions exécutables via le compilateur de vérification d'assertions 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.
* « ESC/Java2 », Extended Static Checker utilise les annotations JML pour effectuer une vérification statique;
* OpenJML, qui effectuer une vérification statique et la vérification d'assertions à l'exécution;
* Daikon, un générateur d'invariant dynamique;
* KeY, un vérificateur manuel de théorèmes;
* Krakatoa, un vérificateur manuel de théorèmes basé sur l'assistant de preuve Coq;
* JMLeclipse, un plugin pour Eclipse l'environnement de développement intégré.