Java Modelling Language: differenze tra le versioni

Versione delle 13:04, 27 ott 2008

Versione delle 14:39, 27 ott 2008

Riga 14:

</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.

===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</code> : The [[universal quantifier]].

:il [[quantificatore universale (simbolo)|quantificatore universale]]

;<code>\exists</code>

:il [[quantificatore esistenziale (simbolo)|quantificatore esistenziale]]

;<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 fspecifiche formali delle proprietà delle classi, dei campi e dei metodi. Un esempio di senmplice annotazione di un metodo potrebbe essere il seguente:

; <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</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 ⟶ 78:

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

}

</langsource>

-->

==Collegamenti esterni==

*[http://www.jmlspecs.org/ Sito ufficiale]