Java Modelling Language: differenze tra le versioni

Versione delle 19:42, 23 lug 2006

Versione attuale delle 14:34, 7 ott 2025

(34 versioni intermedie di 22 utenti non mostrate)

Riga 1:

Il '''Java Modelling Language''' ('''JML''') è un [[linguaggio di specifica]] che permette di definire [[astrazioni procedurali]] su un modello di [[Design by contract|programmazione per contratto]]., E'effettuando disponibiledei solamentecontrolli persui [[JavaParametro (programmazione)|parametri d'ingresso]] 1.4.2di un [[Metodo (programmazione)|metodo]] e sul suo valore di ritorno.

{{stub informatica}}

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.

Il '''Java Modelling Language''' (JML) è un linguaggio che permette di definire [[astrazioni procedurali]] su un modello di [[programmazione per contratto]]. E' disponibile solamente per [[Java]] 1.4.2.

==Sintassi==

{{categoria: ingegneria del software}}

Le specifiche JML sono espresse nella forma

<syntaxhighlight lang=java>

//@ <Specifica JML>

</syntaxhighlight>

oppure

<syntaxhighlight lang=java>

/*@ <Specifica JML> @*/

</syntaxhighlight>

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

:identificatore del valore di ritorno del metodo che segue

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

<syntaxhighlight lang=java>

public class BankingExample {

public static final int MAX_BALANCE = 1000;

private int balance;

private boolean isLocked = false;

//@ invariant balance >= 0 && balance <= MAX_BALANCE;

//@ assignable balance;

//@ ensures balance == 0;

public BankingExample() { ... }

//@ requires amount > 0;

//@ ensures balance = \old(balance) + amount;

//@ assignable balance;

public void credit(int amount) { ... }

//@ requires amount > 0;

//@ ensures balance = \old(balance) - amount;

//@ assignable balance

public void debit(int amount) { ... }

//@ ensures isLocked == true;

public void lockAccount() { ... }

//@ signals (BankingException e) isLocked;

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

}

</syntaxhighlight>

==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}}

{{stub Portale|informatica}}

[[Categoria:Java]]