Java Modelling Language: differenze tra le versioni

Versione delle 14:41, 27 ott 2008

Versione attuale delle 14:34, 7 ott 2025

(19 versioni intermedie di 15 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. È disponibile solamente per [[Piattaforma Java|Java]] 1.4.2.

{{S|informatica}}

'''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. È disponibile solamente per [[Piattaforma Java|Java]] 1.4.2.

Le specifiche vengono aggiunte come [[Annotazione (Java)|annotazioni Java]] all'interno del [[codice sorgente]] [[Java (linguaggio di programmazione)|Java]]., Iltramite codicecommenti JMLdotati sidi scriveuna comespeciale un commento specialesintassi che precedeprecedono 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

<sourcesyntaxhighlight lang=java>

//@ <Specifica JML>

</syntaxhighlight>

</source>

oppure

<sourcesyntaxhighlight lang=java>

/*@ <Specifica JML> @*/

</syntaxhighlight>

</source>

===Direttive===

Riga 21 ⟶ 20:

:definisce una post-condizione sul metodo che segue

;<code>signals</code>

:definisce una condizione in base alla quale deve essere lanciata una [[Gestione delle eccezioni in Java||eccezione]] dal metodo che segue

;<code>assignable</code>

:definisce di quali campi è consentito l'assegnamento dal metodo che segue

Riga 32 ⟶ 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 39 ⟶ 40:

;<code>\old(<name>)</code>

:modificatore con cui riferirsi al valore della variabile <code><name></code> al momento del lancio nel metodo

;<code>(\forall <dominio>;<range_valori>;<condizione> )</code>

:il [[quantificatore universale (simbolo)|quantificatore universale]] su un range di valori in un certo dominio che rispettano una certa condizione.

;<code>(\exists <dominio>;<range_valori>;<condizione> )</code>

:il [[quantificatore esistenziale (simbolo)|quantificatore esistenziale]] su un range di valori in un certo dominio che rispettano una certa condizione.

;<code>a ==> b</code>

:il costrutto logico <code>a</code> implica <code>b</code>

Riga 48 ⟶ 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 fspecifichespecifiche formali delle proprietà delle classi, dei campi e dei metodi. Un esempio di senmplicesemplice annotazione di un metodo potrebbe essere il seguente:

<sourcesyntaxhighlight lang=java>

public class BankingExample {

Riga 78 ⟶ 79:

public /*@ pure @*/ int getBalance() throws BankingException { ... }

}

</syntaxhighlight>

</source>

==Bibliografia==

Riga 85 ⟶ 86:

==Collegamenti esterni==

*[{{cita web|http://www.jmlspecs.org/ |Sito ufficiale]}}

{{Portale|informatica}}

[[Categoria:Linguaggio Java]]

[[en:Java Modeling Language]]

[[fr:Java Modeling Language]]

[[pl:Java Modeling Language]]

[[pt:Java Modeling Language]]