Java Modelling Language

Java Modelling Language (JML) è un linguaggio di specifica che permette di definire astrazioni procedurali su un modello di programmazione per contratto, effettuando dei controlli sui parametri d'ingresso di un metodo e sul suo valore di ritorno. È disponibile solamente per Java 1.4.2.

Le specifiche vengono aggiunte all'interno del codice sorgente Java, tramite commenti dotati di una speciale sintassi che precedono il metodo interessato. Questo significa che il codice JML non viene letto dal compilatore Java, ma solo dagli strumenti di JML.

Sintassi

Le specifiche JML sono espresse nella forma

//@ <Specifica JML>

oppure

 /*@ <Specifica JML> @*/

Direttive

Le direttive principali del linguaggio sono:

requires: definisce una pre-condizione sul metodo che segue
ensures: definisce una post-condizione sul metodo che segue
signals: definisce una condizione in base alla quale deve essere lanciata una eccezione dal metodo che segue
assignable: definisce di quali campi è consentito l'assegnamento dal metodo che segue
pure: dichiara che il metodo che segue non ha effetti collaterali (è un'abbreviazione di assignable \nothing)
invariant: definisce una proprietà invariante della classe
also: dichiara che un metodo deve ereditare le condizioni dalla sua superclasse.
assert: definisce una asserzione JML.
spec_public: Dichiara una variabile pubblica protetta o privata per scopi di specifica.

Espressioni

JML mette a inoltre a disposizione anche le seguenti espressioni:

\result: identificatore del valore di ritorno del metodo che segue
\old(<name>): modificatore con cui riferirsi al valore della variabile <name> al momento del lancio nel metodo
(\forall <dominio>;<range_valori>;<condizione> ): il quantificatore universale su un range di valori in un certo dominio che rispettano una certa condizione.
(\exists <dominio>;<range_valori>;<condizione> ): il quantificatore esistenziale su un range di valori in un certo dominio che rispettano una certa condizione.
a ==> b: il costrutto logico a implica b
a <==> b: il costrutto logico a se e solo se b

Le annotazioni JML hanno inoltre accesso agli oggetti Java, oltre che ai metodi ed agli operatori degli oggetti. Questi sono combinati per fornire specifiche formali delle proprietà delle classi, dei campi e dei metodi. Un esempio di semplice annotazione di un metodo potrebbe essere il seguente:

 public class BankingExample {
 
     public static final int MAX_BALANCE = 1000; 
     private int balance;
     private boolean isLocked = false; 
 
     //@ invariant balance >= 0 && balance <= MAX_BALANCE;
 
     //@ assignable balance;
     //@ ensures balance == 0;
     public BankingExample() { ... }
 
     //@ requires amount > 0;
     //@ ensures balance = \old(balance) + amount;
     //@ assignable balance;
     public void credit(int amount) { ... }
 
     //@ requires amount > 0;
     //@ ensures balance = \old(balance) - amount;
     //@ assignable balance
     public void debit(int amount) { ... }
 
     //@ ensures isLocked == true;
     public void lockAccount() { ... }
 
     //@ signals (BankingException e) isLocked;
     public /*@ pure @*/ int getBalance() throws BankingException { ... }
 }

Bibliografia

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