Java Modelling Language: differenze tra le versioni

Versione delle 12:18, 27 ott 2008

Versione delle 13:04, 27 ott 2008

Riga 13:

/*@ <Specifica JML> @*/

</source>

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.

JML mette 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</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 {

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 { ... }

}

</lang>

-->

==Collegamenti esterni==

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

{{Portale|informatica}}

[[Categoria:Linguaggio Java]]