• Vedi
• Modifica
• Versioni
• Stampa

JML

Java Modeling Language (JML)

Autori: Giorgio Ghisalberti,Vincenzo Manzoni

Introduzione

JML è l'acronimo di Java Modelling Language. E' un insieme di tool e tecniche per il design by contract in Java.

L'idea è quella di utilizzare Java non solo per programmare, ma, aggiungendo al linguaggio dei tool e delle tecniche, anche per modellare. Per far questo, si inseriscono all'interno dei file sorgente delle annotazioni all'interno dei commenti nel file .java. Le annotazioni sono della forma /*@ ... @*/ oppure //@

Le proprietà sono scritte come espressioni boolean di java con alcuni operatori in più: \result, \forall, \old, <==>(se e solo se), ... e alcune parole chiave \requires, \ensures, \invariant,...

Pre & Postconditions

Ecco un esempio di Precondizione per un metodo:

 /*@ requires amount >= 0; 
 ensures balance == \old(balance) -- amount && \result == balance; @*/ 
 public int withdraw(int amount) {
 ...

In questo caso \old(balance) si riferisce al valore di balance prima dell'esecuzione del metodo.

non null

Molti elementi all'interno delle pre e delle postcondizioni spesso devono essere non nulli. L'operatore non null serve proprio per questo motivo.

 public class Directory { 
 private /*@ non null @*/ File[] files; 
 void createSubdir(/*@ non null @*/ String name){ ... }

Assert

La preposizione assert specifica una proprietà che potrebbe essere necessaria in qualche punto del codice. Ad esempio:

 if (i <= 0 || j < 0) { 
 ...
 } else if (j < 5){ 
 //@ assert i > 0 && 0 < j && j < 5; 
 ...
 } else {
 //@ assert i > 0 && j > 5; 
 ... 
 } 

Quantificatori

JML supporta varie forme di quantificatori:

• Universali ed esistenziali (\forall e \exists)
• Quantificatori generali (\sum, \product, \min, \max)
• Quantificatori numerici (\num\_of)

Benefici di JML

Le specifiche JML forniscono una documentazione specifica dei contratti e delle invarianti. Scrivendo JML nel codice è possibile fare assunzioni e considerazioni sparse all'interno del codice.

In questo modo le specifiche JML rendono più semplice la comprensione del codice e aiutano a convincere il programmatore e chi legge il codice che niente può andar storto, ovvero che tutti i possibili errori sono controllati.

Tools per JML

1. JML compiler (jmlc): compila file java per avere class instrumentati
2. JML/Java interpreter (jmlrac):
3. Controllo statico esteso attraverso escjava2
4. JML/JUnit unit test tool (jmlunit)
5. HTML generator (jmldoc)
6. Altri tool

Risorse esterne

• Homepage di JML
• La versione inglese di Wikipedia ha una voce che riguarda JML.