Java Modelling Language: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
null edit: o almeno non sono annotazioni nel senso che il termine "annotazione" ha nelle specifiche di linguaggio JLS 3 |
ho rimosso il fatto che JML fosse disponibile solo per java 1.4.2, informazione senza fonti |
||
| (10 versioni intermedie di 8 utenti non mostrate) | |||
Riga 1:
'''Java Modelling Language''' ('''JML''') è un [[linguaggio di specifica]] che permette di definire astrazioni procedurali su un modello di [[Design by contract|programmazione per contratto]], effettuando dei controlli sui [[Parametro (programmazione)|parametri d'ingresso]] di un [[Metodo (programmazione)|metodo]] e sul suo valore di ritorno
Le specifiche vengono aggiunte all'interno del [[codice sorgente]] [[Java (linguaggio di programmazione)|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>
</syntaxhighlight>
oppure
<
/*@ <Specifica JML> @*/
</syntaxhighlight>
===Direttive===
Riga 31:
;<code>assert</code>
:definisce una asserzione JML.
;<code>spec_public</code>
:Dichiara una variabile pubblica protetta o privata per scopi di specifica.
===Espressioni===
Riga 47 ⟶ 49:
:il costrutto logico <code>a</code> se e solo se <code>b</code>
Le annotazioni JML hanno inoltre accesso agli [[oggetto (informatica)|oggetti]] Java, oltre che ai metodi ed agli [[Operatore (informatica)|operatori]] degli oggetti. Questi sono combinati per fornire specifiche formali delle proprietà delle classi, dei campi e dei metodi. Un esempio di
<
public class BankingExample {
Riga 77 ⟶ 79:
public /*@ pure @*/ int getBalance() throws BankingException { ... }
}
</syntaxhighlight>
==Bibliografia==
Riga 84 ⟶ 86:
==Collegamenti esterni==
*
{{Portale|informatica}}
[[
| |||