Java Modelling Language

Da Wikipedia, l'enciclopedia libera.

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[modifica | modifica sorgente]

Le specifiche JML sono espresse nella forma

//@ <Specifica JML>

oppure

 /*@ <Specifica JML> @*/

Direttive[modifica | modifica sorgente]

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.

Espressioni[modifica | modifica sorgente]

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[modifica | modifica sorgente]

  • (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.

Collegamenti esterni[modifica | modifica sorgente]

informatica Portale Informatica: accedi alle voci di Wikipedia che trattano di informatica