Java Modeling Language

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).

Sommaire

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ées 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 (raccourci pour assignable \nothing).
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 { ... }

}

La documentation complète de la syntaxe JML est disponible ici.

Outils

Il existe de nombreux outils 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, un grand nombre de groupes indépendants travaillent sur des outils utilisant JML. Parmi ceux-ci : ESC/Java2, 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


Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Java Modeling Language de Wikipédia en français (auteurs)

Игры ⚽ Нужно сделать НИР?

Regardez d'autres dictionnaires:

  • Java Modeling Language — The Java Modeling Language (JML) follows the design by contract paradigm. It is a specification language for Java programs, using . There are various verification tools for JML, such as a runtime assertion checker and the Extended Static Checker… …   Wikipedia

  • Java Modeling Language — El Java Modeling Language, abreviado JML y en español «Lenguaje de Modelaje para Java» es un lenguaje de especificación para programas Java, que se sirve de pre , postcondiciones e invariantes de la lógica de Hoare, siguiendo el paradigma de… …   Wikipedia Español

  • Modeling language — A modeling language is any artificial language that can be used to express information or knowledge or systems in a structure that is defined by a consistent set of rules. The rules are used for interpretation of the meaning of components in the… …   Wikipedia

  • Unified Modeling Language — (UML) is a standardized general purpose modeling language in the field of software engineering. UML includes a set of graphical notation techniques to create abstract models of specific systems, referred to as UML model. Overview The Unified… …   Wikipedia

  • Unified Modeling Language — Die Unified Modeling Language (Vereinheitlichte Modellierungssprache), kurz UML, ist eine graphische Modellierungssprache zur Spezifikation, Konstruktion und Dokumentation von Software Teilen und anderen Systemen[1]. Sie wird von der Object… …   Deutsch Wikipedia

  • Unified Modeling Language — Pour les articles homonymes, voir UML. Logo d UML UML (en anglais Unified Modeling Language ou « langage de modélisation unifié ») est un langage de modélisation graphique à base de pictogrammes …   Wikipédia en Français

  • List of Unified Modeling Language tools — This article compares Unified Modeling Language tools. Contents 1 General 2 Features 3 Other UML tools 4 References …   Wikipedia

  • Virtual Reality Modeling Language — VRML im Programm dune (Version 0.13) Die Virtual Reality Modeling Language (VRML) ist eine Beschreibungssprache für 3D Szenen, deren Geometrien, Ausleuchtungen, Animationen und Interaktionsmöglichkeiten inklusive in der virtuellen Umgebung… …   Deutsch Wikipedia

  • Business Process Modeling Language — (BPML) is a meta language for the modeling of business processes, just as XML is a meta language for the modeling of business data. BPML was a proposed language, but now the BPMI has dropped support for this in favor of BPEL4WS. BPMI took this… …   Wikipedia

  • Rational Modeling Language — Ce langage est une abstraction et une modélisation de langage de programmation libre sous licence GNU General Public License, se basant sur la théorie des graphes et la théorie des groupes. Il utilise également les travaux réalisés par le… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”