title: Java Modelling Language
text: # 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
  
  oppure
  
  ### 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:
  
  