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 come annotazioni Java all'interno del codice sorgente Java. Il codice JML si scrive come un commento speciale che precede il metodo, che 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> @*/
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.
JML mette 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