Java Modeling Language

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 diseño por contrato. Las especificaciones se escriben como comentarios de anotación Java en el código fuente, que por consiguiente puede compilarse con cualquier compilador de Java.

Para facilitar el desarrollo existen varias herramientas de verificación, tales como programas que chequean el código antes de su ejecución (ej. ESC/Java).

Contenido

Generalidades

JML es un lenguaje de especificación de interfaz de comportamiento para módulos Java. JML provee una semántica para describir de forma formal el comportamiento de un módulo de Java, evitando así la ambigüedad con respecto a las intenciones del diseñador del módulo. JML ha heredado ideas de Eiffel, Larch y del cálculo de refinamiento, con la meta de proveer una semántica formal rigurosa a la vez que se hace accesible a todo programador de Java. Hay varias herramientas que se sirven de las especificaciones de comportamiento del JML. Dado que las especificaciones se pueden escribir como anotaciones en los archivos de programa de Java, o grabarse en otros archivos de especificación independientes. Los módulos de Java con las especificaciones JML se pueden compilar sin necesidad de cambio alguno con el compilador de Java.

Sintaxis

Las especificaciones JML se agregan al código Java como anotaciones en los comentarios. Los comentarios Java se interpretan entonces como anotaciones JML cuando comienzan con el signo «@». Por ejemplo:

//@ <especificación JML>

o

/*@ <especificación JML> @*/

La sintaxis básica de JML cuenta con las siguientes palabras clave:

requires 
Define una precondición en el método que le sigue.
ensures 
Define una postcondición en el método que le sigue.
signals 
Define una postcondición para cuando se lanza una excepción por el método que le sigue.
signals_only 
Define que excepciones pueden ser lanzadas cuando cuando se da la precondición declarada.
assignable 
Define que campos están permitidos para ser asignados por el método que le sigue.
pure 
Declara un método libre de efectos colaterales (assignable \nothing).
invariant 
Define una propiedad invariante de la clase.
also 
Combina casos de especificación y también puede declarar que un método esta heredando especificaciones de sus supertipos.
assert 
Define una aserción JML.
spec_public 
Declara una variable pública protegida o privada con el fin de una especificación.

El JML básico también provee las siguientes expresiones:

\result 
Un identificador para el valor de retorno de el método que le sigue.
\old(<expression>) 
Un modificador para referirse al valor de la <expression> en el momento de entrada en un método.
(\forall <decl>; <range-exp>; <body-exp>) 
El cuantificador universal.
(\exists <decl>; <range-exp>; <body-exp>) 
El cuantificador existential.
a ==> b 
a implica b
a <== b 
a está implicado por b
a <==> b 
a sólo si b

como cómo la sintaxis Java básica para lógica o para otros propósitos. Las anotaciones JML también tienen objeto a los objetos Java, los métodos de los objetos y operadores que están en el ámbito del método que se anota y que tienen una visibilidad adecuada. Estos se combinan para proveer especificaciones formales de las propiedades de las clases, campos y métodos. Por ejemplo, un ejemplo anotado de una sencilla clase de banco podrías ser así:

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() { balance = 0; }

   //@ requires 0 < amount && amount + balance < MAX_BALANCE;
   //@ assignable balance;
   //@ ensures balance == \old(balance + amount);
   public void credit(int amount) { balance += amount; }

   //@ requires 0 < amount && amount <= balance;
   //@ assignable balance;
   //@ ensures balance == \old(balance) - amount;
   public void debit(int amount) { balance -= amount; }

   //@ ensures isLocked == true;
   public void lockAccount() { isLocked = true; }

   //@   requires !isLocked;
   //@   ensures \result == balance;
   //@ also
   //@   requires isLocked;
   //@   signals_only BankingException;
   public /*@ pure @*/ int getBalance() throws BankingException {
       if (!isLocked) { return balance; }
       else { throw new BankingException(); }
   }
}

La documentación íntegra sobre la sintaxis de JML se puede encontrar en el Manual de referencia de JML.

Herramientas de soporte

Una serie de herramientas proveen funcionalidad basada en las anotaciones JML. Las herramientas de la Iowa State JML otorgan un compilador que verifica las aserciones jmlc que convierte las anotaciones JML en aserciones de tiempo de ejecución, un generador de documentos jmldoc que produce documentación Javadoc ampliada con información extra de las anotaciones JML y un generador de tests de módulos jmlunit que genera un marco para tests JUnit a partir de las anotaciones JML.

También hay grupos independientes que trabajan en herramientas que hacen uso de las anotaciones JML, entre ellas:

  • ESC/Java2 [1], un verificador estático extendido que utiliza anotaciones JML;
  • Daikon, un generador invariante dinámico;
  • KeY, que provee un comprobador de teorema con una fachada JML;
  • Krakatoa, una herramienta de verificación estática basada en la plataforma de verificación Why y utilizando el asistente de evidencia Coq;
  • JMLeclipse, un plugin para el IDE Eclipse con soporte de sintaxis JML e interfaces a varias herramientas que utilizan anotaciones JML.
  • Sireum/Kiasan, un analizador estático basado en una ejecución simbólica que soporta JML como lenguaje de contrato.
  • JMLUnit, una herramienta que genera archivos para ejecutar tests JUnit sobre archivos Java con anotación JML.
  • TACO, programa de análisis de código abierto que estáticamente comprueba el cumplimiento de un programa de Java frente a su especificación en JML.

Referencias

  • Gary T. Leavens and 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, Kluwer, 1999, chapter 12, pages 175-188.
  • Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), September 2009. HTML

Enlaces externos


Wikimedia foundation. 2010.

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

Mira otros diccionarios:

  • 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 — 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… …   Wikipédia en Français

  • 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

Compartir el artículo y extractos

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