Java Modelling Language: differenze tra le versioni

Versione delle 13:04, 27 ott 2008

Versione attuale delle 14:34, 7 ott 2025

(21 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===

Le direttive principali del linguaggio sono:

; <code>requires</code>
: definisce una pre-condizione sul metodo che segue

; <code>ensures</code>
: 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

; <code>pure</code>
: dichiara che il metodo che segue non ha effetti collaterali (è un'abbreviazione di <code>assignable \nothing</code>)

; <code>invariant</code>
: definisce una proprietà invariante della [[Classe (informatica)|classe]]

; <code>also</code>
: dichiara che un metodo deve ereditare le condizioni dalla sua superclasse.

; <code>assert</code>
: definisce una asserzione JML.

;<code>spec_public</code>

:Dichiara una variabile pubblica protetta o privata per scopi di specifica.

===Espressioni===

JML mette a inoltre a disposizione anche le seguenti espressioni:

;<code>\result</code>

; <code>\result</code> : identificatore del valore di ritorno del metodo che segue

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

; <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>

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

: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 semplice annotazione di un metodo potrebbe essere il seguente:

; <code>\result</code> : identificatore del valore di ritorno del metodo che segue

<sourcesyntaxhighlight lang=java>

; <code>\old(<name>)</code> : modificatore con cui riferirsi al valore della variabile <code><name></code> al momento del lancio nel metodo

<!--

; <code>\forall</code> : The [[universal quantifier]].

; <code>\exists</code> : The [[existential quantifier]].

; <code>a ==> b</code> : The logical construct <code>a</code> implies <code>b</code>

; <code>a <==> b</code> : The logical construct <code>a</code> if and only if <code>b</code>

as well as standard [[Java syntax]] for logical and, or, and not. JML annotations also have access to Java objects, object methods and operators that are within the scope of the method being annotated. These are combined to provide formal specifications of the properties of classes, fields and methods. For example, an annotated example of a simple banking class may look like

<source lang=java>

public class BankingExample {

Riga 64 ⟶ 79:

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

}

</syntaxhighlight>

</lang>

-->

==Bibliografia==

* {{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==

*[{{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]]